distribution_czOperatorBound

lemma distribution_czOperatorBound (ha : 4 ≤ a) (hf : BoundedFiniteSupport f)    (hα : ⨍⁻ x, ‖f x‖ₑ / c10_0_3 a < α) (hX : GeneralCase f (α' a α)) :    volume ((Ω f (α' a α))ᶜ ∩ czOperatorBound hX ⁻¹' Ioi (α / 8)) ≤    C10_2_8 a / α * eLpNorm f 1 volume := by  rcases eq_zero_or_pos α with rfl | αpos; · simp at hα  rcases eq_top_or_lt_top α with rfl | αlt  · have : czOperatorBound hX ⁻¹' Ioi (⊤ / 8) = ∅ := by      rw [top_div_of_ne_top (by norm_num), isMax_top.Ioi_eq, preimage_empty]    rw [this, inter_empty, measure_empty]; exact zero_le  calc    _ ≤ (volume.restrict (Ω f (α' a α))ᶜ) {x | α / 8 ≤ czOperatorBound hX x} := by      rw [inter_comm, ← Measure.restrict_apply']; swap      · apply MeasurableSet.compl; simp_rw [Ω, hX, dite_true]        exact MeasurableSet.iUnion fun _ ↦ measurableSet_ball      gcongr; intro x mx; simp only [mem_preimage, mem_Ioi, mem_setOf_eq] at mx ⊢; exact mx.le    _ ≤ (∫⁻ x in (Ω f (α' a α))ᶜ, czOperatorBound hX x) / (α / 8) := by      apply meas_ge_le_lintegral_div      · refine ((AEMeasurable.tsum fun i ↦ ?_).const_mul _).restrict        refine AEMeasurable.div ?_ measurable_vol₁.aemeasurable        refine ((AEMeasurable.const_div ?_ _).pow_const _).mul_const _        simp only [coe_nnreal_ennreal_nndist]        exact aemeasurable_id'.edist aemeasurable_const      · simp [αpos.ne']      · finiteness    _ ≤ 8 * C10_2_7 a * ∑' i, volume (czBall3 hX i) * ∫⁻ x in (Ω f (α' a α))ᶜ,        ((3 * czRadius hX i).toNNReal / edist x (czCenter hX i)) ^ (a : ℝ)⁻¹ /        volume (ball x (dist x (czCenter hX i))) := by      unfold czOperatorBound      rw [lintegral_const_mul' _ _ (by finiteness), ENNReal.div_eq_inv_mul,        ENNReal.inv_div (.inr αlt.ne) (.inr αpos.ne'), ← mul_assoc, ← mul_assoc,        ← ENNReal.mul_div_right_comm, ENNReal.div_mul_cancel αpos.ne' αlt.ne]      simp only [coe_nnreal_ennreal_nndist]      rw [lintegral_tsum]; swap      · refine fun i ↦ (AEMeasurable.div ?_ measurable_vol₁.aemeasurable).restrict        refine ((AEMeasurable.const_div ?_ _).pow_const _).mul_const _        exact aemeasurable_id'.edist aemeasurable_const      congr! 3 with i      rw [← lintegral_const_mul' _ _ (by finiteness)]; congr 2 with x      rw [← ENNReal.mul_comm_div, mul_div_assoc, mul_comm]    _ ≤ 8 * C10_2_7 a * ∑' i, volume (czBall3 hX i) * 2 ^ (3 * a) := by      gcongr with i; exact czOperatorBound_inner_le ha hX    _ ≤ 8 * C10_2_7 a * 2 ^ (3 * a) * (2 ^ (4 * a) / α' a α * eLpNorm f 1 volume) := by      rw [ENNReal.tsum_mul_right, mul_comm _ (2 ^ _), ← mul_assoc]; gcongr      exact tsum_volume_czBall3_le hf hX (α'_pos αpos)    _ = _ := by      rw [← mul_assoc, ← mul_div_assoc, show (8 : ℝ≥0∞) * C10_2_7 a * 2 ^ (3 * a) * 2 ^ (4 * a) =        2 ^ (7 * a + 3) * C10_2_7 a by ring, C10_2_7, coe_mul, ← mul_assoc, div_α'_eq,        ENNReal.mul_div_cancel_right (by rw [c10_0_3]; positivity) (by rw [c10_0_3]; finiteness),        show (2 : ℝ≥0∞) = (2 : ℝ≥0) by rfl, ← coe_pow, ← coe_mul, ← pow_add, C10_2_8]      congr 4; ring