cotlar_control

theorem cotlar_control (ha : 4 ≤ a) {g : X → ℂ} (hg : BoundedFiniteSupport g) (hr : r ∈ Ioc 0 R)    (hx : dist x x' ≤ R / 4) :    ‖czOperator K R g x‖ₑ ≤ ‖czOperator K r ((ball x (R / 2))ᶜ.indicator g) x'‖ₑ +    C10_1_3 a * globalMaximalFunction volume 1 g x := by  have R_pos : 0 < R := by    rw [mem_Ioc] at hr    linarith  calc ‖czOperator K R g x‖ₑ    _ = ‖(czOperator K R g x - czOperator K R g x') + czOperator K R g x'‖ₑ := by      congr      ring    _ ≤ ‖czOperator K R g x - czOperator K R g x'‖ₑ + ‖czOperator K R g x'‖ₑ := by      apply enorm_add_le    _ = nndist (czOperator K R g x) (czOperator K R g x') + ‖czOperator K R ((ball x (R / 2))ᶜ.indicator g) x'‖ₑ := by      rw [enorm_eq_nnnorm, ← nndist_eq_nnnorm, cut_out_ball hr hx]    _ ≤ C10_1_2 a * globalMaximalFunction volume 1 g x + (‖czOperator K r ((ball x (R / 2))ᶜ.indicator g) x' - czOperator K R ((ball x (R / 2))ᶜ.indicator g) x'‖ₑ + ‖czOperator K r ((ball x (R / 2))ᶜ.indicator g) x'‖ₑ) := by      gcongr      · apply estimate_x_shift ha hg R_pos        linarith      · --triangle inequality as above        rw [← edist_eq_enorm_sub, edist_comm, edist_eq_enorm_sub]        apply le_trans _ (enorm_add_le _ _)        apply le_of_eq        congr        ring    _ ≤ C10_1_2 a * globalMaximalFunction volume 1 g x + 2 ^ (a ^ 3 + 4 * a) * globalMaximalFunction volume 1 g x + ‖czOperator K r ((ball x (R / 2))ᶜ.indicator g) x'‖ₑ := by      rw [add_assoc]      gcongr      exact radius_change hg hr hx    _ ≤ ‖czOperator K r ((ball x (R / 2))ᶜ.indicator g) x'‖ₑ + C10_1_3 a * globalMaximalFunction volume 1 g x := by      rw [add_comm]      gcongr      rw [← add_mul]      gcongr      rw [C10_1_2_def, C10_1_3_def]      norm_num      calc (2 : ℝ≥0∞) ^ (a ^ 3 + 2 * a + 2) + 2 ^ (a ^ 3 + 4 * a)        _ = (2 : ℝ≥0∞) ^ (a ^ 3 + (2 * a + 2)) + 2 ^ (a ^ 3 + 4 * a) := by          congr 1        _ ≤ 2 ^ (a ^ 3 + 4 * a) + 2 ^ (a ^ 3 + 4 * a) := by          gcongr          · exact one_le_two          · linarith        _ = 2 * 2 ^ (a ^ 3 + 4 * a) := (two_mul (2 ^ (a ^ 3 + 4 * a))).symm        _ = 2 ^ (a ^ 3 + 4 * a + 1) := (pow_succ' 2 (a ^ 3 + 4 * a)).symm