cotlar_estimate

theorem cotlar_estimate (ha : 4 ≤ a)    (hT : ∀ r > 0, HasBoundedStrongType (czOperator K r) 2 2 volume volume (C_Ts a))    {g : X → ℂ} (hg : BoundedFiniteSupport g) (hr : r ∈ Ioc 0 R) :    ‖czOperator K R g x‖ₑ ≤ 4 * globalMaximalFunction volume 1 (czOperator K r g) x +      C10_1_5 a * globalMaximalFunction volume 1 g x := by  let F1 : Set X := {x' | 4 * globalMaximalFunction volume 1 (czOperator K r g) x < ‖czOperator K r g x'‖ₑ}  let F2 : Set X := {x' | ↑(C10_1_4 a) * globalMaximalFunction volume 1 g x < ‖czOperator K r ((ball x (R / 2)).indicator g) x'‖ₑ}  let noF : Set X := (F1 ∪ F2)ᶜ ∩ ball x (R / 4)  have vF1F2 : volume.restrict (ball x (R / 4)) (F1 ∪ F2) ≤ volume (ball x (R / 4)) / 2 := by    apply le_trans (measure_union_le F1 F2)    have vF1 := cotlar_set_F₁ (K := K) (x := x) hr.1 hr.2 hg    have vF2 := cotlar_set_F₂ (K := K) (x := x) ha hr.1 hr.2 hT hg    unfold F1 F2    apply le_of_le_of_eq (add_le_add vF1 vF2)    rw [← mul_two, div_eq_mul_inv, div_eq_mul_inv, div_eq_mul_inv, mul_assoc]    congr    apply ENNReal.eq_inv_of_mul_eq_one_left    have : (2 : ℝ≥0∞) * 2 = 4 := by ring    rw [mul_assoc, this, ENNReal.inv_mul_cancel (by simp) (by simp)]  have : noF.Nonempty := by    apply nonempty_of_measure_ne_zero (μ := volume)    intro hnoF    have : (2 : ℝ≥0∞) ≤ 1 := by      rw [← ENNReal.mul_le_mul_iff_right (a := volume (ball x (R / 4))) ?ne_z (by finiteness), mul_one]      case ne_z => apply ne_of_gt; apply measure_ball_pos; linarith [lt_of_lt_of_le hr.1 hr.2]      have := measure_univ_le_add_compl (μ := volume.restrict (ball x (R / 4))) (s := F1 ∪ F2)      nth_rw 3 [Measure.restrict_apply' measurableSet_ball] at this      rw [hnoF, add_zero, Measure.restrict_apply_univ] at this      exact (ENNReal.le_div_iff_mul_le (by simp) (by simp)).mp (this.trans vF1F2)    exact Nat.not_ofNat_le_one this  obtain ⟨x', hx'⟩ := this  have hxx' := mem_ball.mp hx'.2  rw [dist_comm] at hxx'  apply cotlar_control ha hg hr hxx'.le |> le_trans  rw [indicator_compl, czOperator_sub hg (hg.indicator measurableSet_ball) hr.1, Pi.sub_apply]  have h1x' : ‖czOperator K r g x'‖ₑ ≤ 4 * globalMaximalFunction volume 1 (czOperator K r g) x := by    suffices x' ∉ F1 by      rw [notMem_setOf_iff, not_lt] at this      exact this    exact notMem_subset subset_union_left ((mem_compl_iff _ _).mp hx'.1)  have h2x' : ‖czOperator K r ((ball x (R / 2)).indicator g) x'‖ₑ ≤ C10_1_4 a * globalMaximalFunction volume 1 g x := by    suffices x' ∉ F2 by      rw [notMem_setOf_iff, not_lt] at this      exact this    exact notMem_subset subset_union_right ((mem_compl_iff _ _).mp hx'.1)  apply add_le_add (add_le_add h1x' h2x' |> enorm_sub_le.trans) (by rfl) |> le_trans  rw [add_assoc, C10_1_3_def, C10_1_4_def, C10_1_5_def, ← add_mul]  conv_rhs => rw [pow_succ, mul_two]  push_cast  gcongr _ + (_ + 2 ^ ?_) * _  · exact one_le_two  · lia