estimate_czOperator

lemma estimate_czOperator (ha : 4 ≤ a) (hr : 0 < r) (hf : BoundedFiniteSupport f)    (hT : HasBoundedStrongType (czOperator K r) 2 2 volume volume (C_Ts a)) :    distribution (czOperator K r f) α volume ≤ C10_0_3 a / α * eLpNorm f 1 volume := by  rcases le_or_gt α (⨍⁻ x, ‖f x‖ₑ / c10_0_3 a) with hα | hα  · rw [laverage_eq] at hα    rcases eq_zero_or_pos (eLpNorm f 1) with hf₂ | hf₂    · rw [eLpNorm_eq_zero_iff hf.aestronglyMeasurable one_ne_zero] at hf₂      have op0 : czOperator K r f = 0 := by        ext x; rw [czOperator, integral_eq_zero_of_ae]; swap        · have := (EventuallyEq.rfl (f := (K x ·))).mul hf₂          simp only [mul_zero] at this; exact this.restrict        simp      simp_rw [op0, distribution, Pi.zero_apply, enorm_zero, not_lt_zero, setOf_false,        measure_empty, zero_le]    conv_rhs at hα =>      enter [1, 2, x]; rw [div_eq_mul_inv, c10_0_3, coe_inv (by positivity), inv_inv]    rw [lintegral_mul_const' _ _ (by finiteness), ← eLpNorm_one_eq_lintegral_enorm] at hα    replace hα := mul_le_of_le_div' hα    rw [← ENNReal.le_div_iff_mul_le] at hα; rotate_left    · right; positivity    · have hf₃ := (hf.memLp 1).eLpNorm_lt_top      right; finiteness    rw [mul_comm, ENNReal.mul_div_right_comm] at hα    refine (measure_mono (subset_univ _)).trans (hα.trans ?_)    rw [C10_0_3, add_assoc]; gcongr; exacts [one_le_two, by lia]  rcases eq_zero_or_pos α with rfl | αpos; · simp only [_root_.not_lt_zero] at hα  have α'pos : 0 < c10_0_3 a * α := by rw [c10_0_3]; positivity  calc    _ ≤ distribution (czOperator K r (czApproximation f (α' a α))) (α / 2) volume +        distribution (czOperator K r (czRemainder f (α' a α))) (α / 2) volume := by      refine le_trans (measure_mono fun x mx ↦ ?_) (measure_union_le _ _)      simp only [mem_union, mem_setOf_eq] at mx ⊢; contrapose! mx      calc        _ = ‖czOperator K r (czApproximation f (α' a α)) x +            czOperator K r (czRemainder f (α' a α)) x‖ₑ := by          congr 1; rw [← sub_eq_iff_eq_add']          have key := congrFun (czOperator_sub (K := K) hf (hf.czApproximation α'pos) hr) x          rw [Pi.sub_apply] at key; exact key.symm        _ ≤ _ := enorm_add_le _ _        _ ≤ _ := add_le_add mx.1 mx.2        _ = _ := ENNReal.add_halves α    _ ≤ C10_2_6 a / α * eLpNorm f 1 volume + C10_2_9 a / α * eLpNorm f 1 volume :=      add_le_add (estimate_good hf hα hT) (estimate_bad ha hr hf hα)    _ ≤ _ := by      rw [← add_mul, ← ENNReal.add_div, ← coe_add]; gcongr      calc        _ = 2 ^ (a ^ 3 - 9 * a - 2 : ℤ) + C10_2_9 a := by          rw [C10_2_6, c10_0_3, ← zpow_natCast, ← zpow_natCast, ← zpow_neg, ← zpow_add₀ two_ne_zero]          congr 2; push_cast; ring        _ ≤ 2 ^ a ^ 3 + 2 ^ (5 * a) * 2 ^ (a ^ 3 + 12 * a + 4) + 2 ^ (a ^ 3 + 9 * a + 4) := by          rw [C10_2_9, ← add_assoc, c10_0_3, div_inv_eq_mul, C10_2_8]; gcongr          rw [← zpow_natCast, Nat.cast_pow]          gcongr          · exact one_le_two          · lia        _ ≤ 3 * 2 ^ (a ^ 3 + 17 * a + 4) := by          rw [← pow_add, show 5 * a + (a ^ 3 + 12 * a + 4) = a ^ 3 + 17 * a + 4 by ring,            show (3 : ℝ≥0) = 1 + 1 + 1 by norm_num]          simp_rw [add_mul, one_mul]; gcongr          · exact one_le_two          · linarith          · exact one_le_two          · norm_num        _ ≤ 2 ^ (a ^ 3 + 17 * a + 6) := by          rw [show a ^ 3 + 17 * a + 6 = 2 + (a ^ 3 + 17 * a + 4) by ring, pow_add _ 2]          gcongr; norm_num        _ ≤ _ := by rw [C10_0_3, add_assoc]; gcongr; exacts [one_le_two, by lia]