eLpNorm_czRemainder'_le

lemma eLpNorm_czRemainder'_le {hf : BoundedFiniteSupport f} {hX : GeneralCase f α}    {i : ℕ} :    eLpNorm (czRemainder' hX i) 1 volume ≤ 2 ^ (2 * a + 1) * α * volume (czBall3 hX i) := by  by_cases hi : czRadius hX i ≤ 0  · simp [czRemainder'_eq_zero hX hi]  calc    _ ≤ 2 * (∫⁻ x in czPartition hX i, ‖f x‖ₑ) := ineq_10_2_32 hf    _ ≤ 2 * (volume (czBall7 hX i) * α) := by      apply mul_le_mul_right ∘ (le_trans <| lintegral_mono_set czPartition_subset_czBall7)      have h : volume (czBall7 hX i) ≠ 0 :=        measure_ball_pos _ _ (mul_pos Nat.ofNat_pos (lt_of_not_ge hi)) |>.ne'      simpa [laverage, ENNReal.inv_mul_le_iff h measure_ball_ne_top] using laverage_czBall7_le hX i    _ ≤ 2 * ((volume (ball (czCenter hX i) (2 ^ 2 * (3 * czRadius hX i)))) * α) := by      gcongr; convert czBall_subset_czBall (b := 7) (c := 12) using 2; ring    _ ≤ 2 * (2 ^ (2 * a) * volume (czBall3 hX i) * α) := by      gcongr;      exact (measure_ball_two_le_same_iterate _ _ 2).trans_eq <| by simp [pow_mul, mul_comm 2]    _ = 2 ^ (2 * a + 1) * α * volume (czBall3 hX i) := by ring