estimate_bad

lemma estimate_bad (ha : 4 ≤ a) (hr : 0 < r)    (hf : BoundedFiniteSupport f) (hα : ⨍⁻ x, ‖f x‖ₑ / c10_0_3 a < α) :    distribution (czOperator K r (czRemainder f (α' a α))) (α / 2) volume ≤    C10_2_9 a / α * eLpNorm f 1 volume := by  rcases eq_zero_or_pos α with rfl | αpos; · simp only [not_lt_zero] at hα  by_cases hX : GeneralCase f (α' a α)  · calc      _ ≤ volume (Ω f (α' a α) ∪          {x ∈ (Ω f (α' a α))ᶜ | α / 2 < ‖czOperator K r (czRemainder f (α' a α)) x‖ₑ}) := by        refine measure_mono fun x mx ↦ ?_        rw [mem_setOf_eq] at mx        simp_rw [mem_union, mem_setOf_eq, mx, and_true, mem_compl_iff]; tauto      _ ≤ volume (Ω f (α' a α)) +          volume {x ∈ (Ω f (α' a α))ᶜ | α / 2 < ‖czOperator K r (czRemainder f (α' a α)) x‖ₑ} :=        measure_union_le _ _      _ ≤ ∑' i, volume (czBall6 hX i) +          volume ((Ω f (α' a α))ᶜ ∩ czOperatorBound hX ⁻¹' Ioi (α / 8)) := by        gcongr        · simp_rw [Ω, hX, dite_true]; exact measure_iUnion_le _        · intro x mx; simp_rw [mem_setOf_eq, mem_inter_iff, mem_preimage, mem_Ioi] at mx ⊢          obtain ⟨mx₁, mx₂⟩ := mx; refine ⟨mx₁, ?_⟩; contrapose! mx₂          calc            _ ≤ 3 * czOperatorBound hX x + α / 8 := estimate_bad_partial hf hr hα mx₁ hX            _ ≤ 3 * (α / 8) + α / 8 := by gcongr            _ = _ := by              rw [← add_one_mul, show (3 : ℝ≥0∞) + 1 = 4 by norm_num,                show (8 : ℝ≥0∞) = 4 * 2 by norm_num, ← mul_div_assoc,                ENNReal.mul_div_mul_left _ _ (by norm_num) (by norm_num)]      _ ≤ 2 ^ a * ∑' i, volume (czBall3 hX i) + C10_2_8 a / α * eLpNorm f 1 volume := by        rw [← ENNReal.tsum_mul_left]; gcongr with i        · rw [czBall6, czBall3, show (6 : ℝ) = 2 * 3 by norm_num, mul_assoc]          convert! measure_ball_two_le_same (μ := volume) (czCenter hX i) (3 * czRadius hX i)          unfold defaultA; norm_cast        · exact distribution_czOperatorBound ha hf hα hX      _ ≤ 2 ^ (5 * a) / α' a α * eLpNorm f 1 volume + C10_2_8 a / α * eLpNorm f 1 volume := by        rw [show 5 * a = a + 4 * a by ring, pow_add, mul_div_assoc, mul_assoc]; gcongr        exact tsum_volume_czBall3_le hf hX (α'_pos αpos)      _ = _ := by        nth_rw 1 [← add_mul, div_α'_eq, ← ENNReal.add_div, show (2 : ℝ≥0∞) = (2 : ℝ≥0) by rfl,          ← coe_pow, ← coe_div (by rw [c10_0_3]; positivity), ← coe_add, C10_2_9]  · calc      _ ≤ volume (univ : Set X) := measure_mono (subset_univ _)      _ ≤ 2 ^ (2 * a) / α' a α * eLpNorm f 1 volume := volume_univ_le hf hX (α'_pos αpos)      _ ≤ 2 ^ (5 * a) / c10_0_3 a / α * eLpNorm f 1 volume := by rw [div_α'_eq]; gcongr <;> norm_num      _ ≤ _ := by        rw [show (2 : ℝ≥0∞) = (2 : ℝ≥0) by rfl, ← coe_pow, ← coe_div (by rw [c10_0_3]; positivity),          C10_2_9]        gcongr; exact le_self_add