simple_nontangential_operator

theorem simple_nontangential_operator (ha : 4 ≤ a)    (hT : ∀ r > 0, HasBoundedStrongType (czOperator K r) 2 2 volume volume (C_Ts a)) (hr : 0 < r) :    HasBoundedStrongType (simpleNontangentialOperator K r) 2 2 volume volume (C10_1_6 a) := by  intro g hg  constructor  · exact aestronglyMeasurable_simpleNontangentialOperator  let pointwise : X → ℝ≥0∞ :=    4 * globalMaximalFunction volume 1 (czOperator K r g) + C10_1_5 a • globalMaximalFunction volume 1 g +    C10_1_2 a • globalMaximalFunction volume 1 g  trans eLpNorm pointwise 2 volume  · apply eLpNorm_mono_enorm    simp_rw [enorm_eq_self, simpleNontangentialOperator, iSup_le_iff]    intro x R hR x' hx'    rw [mem_ball, dist_comm] at hx'    trans ‖czOperator K R g x‖ₑ + C10_1_2 a * globalMaximalFunction volume 1 g x    · calc ‖czOperator K R g x'‖ₑ        _ = ‖czOperator K R g x + (czOperator K R g x' - czOperator K R g x)‖ₑ := by congr; ring      apply le_trans <| enorm_add_le _ _      gcongr      rw [← edist_eq_enorm_sub, edist_comm]      exact estimate_x_shift ha hg (hr.trans hR.lt) hx'.le    apply add_le_add (cotlar_estimate ha hT hg ?hrR) (by rfl)    case hrR => rw [mem_Ioc]; exact ⟨hr, hR.le⟩  unfold pointwise  have hst_gmf : HasStrongType (globalMaximalFunction (X := X) (E := ℂ) volume 1) 2 2 _ _ _ :=    hasStrongType_maximalFunction (p₁ := 1) zero_lt_one one_lt_two  norm_cast at hst_gmf  have hst_gmf_g := hst_gmf g (hg.memLp 2)  have aesm_gmf_g := hst_gmf_g.1 -- for fun_prop  have hst_gmf_czg := hst_gmf (czOperator K r g) ((hT r hr).memLp hg)  have aesm_gmf_czg := hst_gmf_czg.1 -- for fun_prop  rw [show 4 * globalMaximalFunction volume 1 (czOperator K r g) =      (4 : ℝ≥0) • globalMaximalFunction volume 1 (czOperator K r g) by rfl]  apply le_trans <| eLpNorm_add_le (by fun_prop) (by fun_prop) one_le_two  apply le_trans <| add_le_add (eLpNorm_add_le (by fun_prop) (by fun_prop) one_le_two) (by rfl)  rw [    show eLpNorm ((4 : ℝ≥0) • globalMaximalFunction volume 1 (czOperator K r g)) 2 volume = ‖(4 : ℝ≥0)‖ₑ * eLpNorm (globalMaximalFunction volume 1 (czOperator K r g)) 2 volume from eLpNorm_const_smul',    show eLpNorm (C10_1_5 a • globalMaximalFunction volume 1 g) 2 volume = ‖C10_1_5 a‖ₑ * eLpNorm (globalMaximalFunction volume 1 g) 2 volume from eLpNorm_const_smul',    show eLpNorm (C10_1_2 a • globalMaximalFunction volume 1 g) 2 volume = ‖C10_1_2 a‖ₑ * eLpNorm (globalMaximalFunction volume 1 g) 2 volume from eLpNorm_const_smul',    enorm_NNReal, enorm_NNReal, enorm_NNReal, add_assoc, ← add_mul  ]  apply le_trans <| add_le_add    (mul_le_mul_right (hst_gmf_czg.2.trans <| mul_le_mul_right (hT r hr g hg).2 _) _)    (mul_le_mul_right hst_gmf_g.2 _)  nth_rw 3 [← mul_assoc]; nth_rw 2 [← mul_assoc]; rw [← mul_assoc, ← add_mul]  gcongr  -- what remains is constant manipulation  nth_rw 2 [mul_comm]; rw [← mul_assoc, ← add_mul]  norm_cast  have : C2_0_6 (defaultA a) 1 2 ≤ 2 ^ (4 * a + 1) := by    rw [C2_0_6_defaultA_one_two_eq, ← NNReal.rpow_natCast]    apply NNReal.rpow_le_rpow_of_exponent_le one_le_two    trans 3 * a + 2    · linarith    norm_cast    linarith [ha]  apply le_trans <| mul_le_mul_right this _  rw [C10_1_6_def, C_Ts, C10_1_5, C10_1_2]  norm_cast  rw [show a ^ 3 + 24 * a + 6 = (a ^ 3 + 20 * a + 5) + (4 * a + 1) by ring]; nth_rw 4 [pow_add]  gcongr  nth_rw 6 [pow_succ]; rw [mul_two]  apply add_le_add  · ring_nf; gcongr <;> simp [Nat.one_le_pow]  nth_rw 5 [pow_succ]; rw [mul_two]  gcongr _ + 2 ^ ?_  · exact one_le_two  · lia