nontangential_from_simple

theorem nontangential_from_simple (ha : 4 ≤ a)    (hT : ∀ r > 0, HasBoundedStrongType (czOperator K r) 2 2 volume volume (C_Ts a)) :    HasBoundedStrongType (nontangentialOperator K) 2 2 volume volume (C10_0_2 a) := by  intro g hg  have eLpNorm_sno_le := simple_nontangential_operator_le ha hT le_rfl g hg |>.2  constructor  · exact aestronglyMeasurable_nontangentialOperator  trans ENNReal.ofNNReal (2 * C10_1_6 a) * eLpNorm g 2 volume  · push_cast; rw [two_mul, add_mul]    apply le_trans _ <| add_le_add eLpNorm_sno_le eLpNorm_sno_le    rw [← two_mul]    apply eLpNorm_le_nnreal_smul_eLpNorm_of_ae_le_mul'    simp_rw [nontangential_operator_boundary hg, enorm_eq_self]    filter_upwards with x    have {R₁ R₂ : ℝ} (hR1 : 0 < R₁) (hR1R2 : R₁ < R₂) {x' : X} : ‖∫ (y : X) in ball x' R₂ \ ball x' R₁, K x' y * g y‖ₑ ≤        ‖∫ (y : X) in (ball x' R₁)ᶜ, K x' y * g y‖ₑ +        ‖∫ (y : X) in (ball x' R₂)ᶜ, K x' y * g y‖ₑ := by      apply le_trans _ enorm_sub_le      have : (ball x' R₁)ᶜ = (ball x' R₂)ᶜ ∪ (ball x' R₂ \ ball x' R₁) := by        rw [compl_eq_univ_sdiff, ← union_compl_self <| ball x' R₂, union_sdiff_distrib, union_comm]        congr        rw [sdiff_eq_compl_inter, inter_eq_right, compl_subset_compl]        exact ball_subset_ball hR1R2.le      rw [this, setIntegral_union_2 (disjoint_compl_left_iff_subset.mpr sdiff_subset) (by measurability)        (by rw [← this]; exact czOperator_welldefined (K := K) hg hR1 x')]      simp    trans ⨆ (R₂ : ℝ) (R₁ ∈ Ioo 0 R₂) (x' ∈ ball x R₁),        ‖∫ (y : X) in (ball x' R₁)ᶜ, K x' y * g y‖ₑ + ‖∫ (y : X) in (ball x' R₂)ᶜ, K x' y * g y‖ₑ    · gcongr with R₂ R₁ hR₁      exact this hR₁.1 hR₁.2    have {R : ℝ} (hR : 0 < R) {x' : X} (hx' : dist x' x <  R) :        ‖∫ (y : X) in (ball x' R)ᶜ, K x' y * g y‖ₑ ≤ simpleNontangentialOperator K 0 g x := by      unfold simpleNontangentialOperator czOperator      apply le_trans _ <| le_iSup _ R; rw [iSup_pos hR]      apply le_trans _ <| le_iSup _ x'; rw [← mem_ball] at hx'; rw [iSup_pos hx']    rw [iSup_le_iff]; intro R₂    rw [iSup₂_le_iff]; intro R₁ hR₁    rw [iSup₂_le_iff]; intro x' hx'    norm_cast; rw [two_mul]    exact add_le_add (this hR₁.1 hx') (this (hR₁.1.trans hR₁.2) (hx'.trans hR₁.2))  · rw [C10_1_6, C10_0_2, ← pow_succ']; gcongr; · exact one_le_two    calc      _ ≤ a ^ 3 + 2 * 4 * 4 * a := by lia      _ ≤ a ^ 3 + 2 * a * a * a := by gcongr      _ = _ := by ring