simple_nontangential_operator_le

theorem simple_nontangential_operator_le (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  by_cases h : 0 < r  · exact simple_nontangential_operator ha hT h  have : r = 0 := by linarith  rw [this]  intro g hg  constructor  · exact aestronglyMeasurable_simpleNontangentialOperator  let f (n : ℕ) := simpleNontangentialOperator K (n + 1 : ℝ)⁻¹ g  have f_mon (x : X): Monotone fun n ↦ f n x := by    intro m n hmn; simp only    unfold f simpleNontangentialOperator    gcongr with R    simp_rw [gt_iff_lt]    apply iSup_const_mono (lt_of_le_of_lt _)    rw [inv_le_inv₀ (by positivity) (by positivity)]    simp [hmn]  have snt0 : (fun x => ⨆ (n : ℕ), f n x) = simpleNontangentialOperator K 0 g := by    ext x    unfold f simpleNontangentialOperator    simp_rw [gt_iff_lt]; rw [iSup_comm]    congr with R    apply le_antisymm (iSup_le <| fun n ↦ iSup_const_mono (lt_trans (by positivity))) (iSup_le _)    intro hR    let n := Nat.ceil R⁻¹    have hn : (n + 1 : ℝ)⁻¹ < R := inv_lt_of_inv_lt₀ hR <| Nat.le_ceil R⁻¹ |>.trans_lt (by linarith)    let seq (n : ℕ) := ⨆ (_ : (n + 1 : ℝ)⁻¹ < R), ⨆ x' ∈ ball x R, ‖czOperator K R g x'‖ₑ    have : ⨆ x' ∈ ball x R, ‖czOperator K R g x'‖ₑ = seq n := by unfold seq; rw [iSup_pos hn]    nth_rw 1 [this]    exact le_iSup seq n  have mct := eLpNorm_iSup' (p := 2) (f := f) (μ := volume)    (fun n ↦ aestronglyMeasurable_simpleNontangentialOperator.aemeasurable)    (by filter_upwards; exact f_mon)  rw [← snt0, mct]  apply iSup_le  intro n; unfold f  apply simple_nontangential_operator ha hT (by positivity) g hg |>.2