nontangential_operator_boundary

theorem nontangential_operator_boundary {f : X → ℂ} (hf : BoundedFiniteSupport f) :    nontangentialOperator K f x =    ⨆ (R₂ : ℝ) (R₁ ∈ Ioo 0 R₂) (x' ∈ ball x R₁),      ‖∫ y in ball x' R₂ \ ball x' R₁, K x' y * f y‖ₑ := by  let sup : ℝ≥0∞ := ⨆ (R₂ : ℝ) (R₁ ∈ Ioo 0 R₂) (x' ∈ ball x R₁),    ‖∫ y in ball x' R₂ \ ball x' R₁, K x' y * f y‖ₑ  unfold nontangentialOperator  apply le_antisymm  all_goals (    rw [iSup_le_iff]; intro R₂    rw [iSup₂_le_iff]; intro R₁ hR₁    rw [iSup₂_le_iff]; intro x' hx'  )  · have (R' : ℝ) (hR' : R' ∈ Ioo R₁ R₂) : ‖∫ (y : X) in Annulus.oo x' R₁ R₂, K x' y * f y‖ₑ ≤        ‖∫ (y : X) in Annulus.oo x' R₁ R', K x' y * f y‖ₑ + sup := by      have : Annulus.oo x' R₁ R₂ = Annulus.oo x' R₁ R' ∪ Annulus.co x' R' R₂ :=        Annulus.oo_union_co hR'.1 hR'.2.le |>.symm      rw [this, setIntegral_union_2 (disjoint_left.mpr <| fun x hx hx2 ↦ not_lt.mpr hx2.1 hx.2)        (by measurability)]; swap      · simp_rw [← this]        apply IntegrableOn.mono_set <| czOperator_welldefined hf hR₁.1 x'        rw [← Annulus.ci_eq]        exact Annulus.oo_subset_ci (by rfl)      apply le_trans <| enorm_add_le _ _      gcongr      rw [Annulus.co_eq, inter_comm, ← sdiff_eq_compl_inter]      refine le_iSup_of_le ?_ (i := R₂)      refine le_iSup₂_of_le ?_ (i := R') (j := ⟨hR₁.1.trans hR'.1, hR'.2⟩)      refine le_iSup₂_of_le ?_  (i := x') (j := hx'.trans hR'.1)      rfl    -- apply continuity    have le_R1 : ‖∫ (y : X) in Annulus.oo x' R₁ R₂, K x' y * f y‖ₑ ≤        ‖∫ (y : X) in Annulus.oo x' R₁ R₁, K x' y * f y‖ₑ + sup := by      refine ContinuousWithinAt.closure_le ?_ ?_ ?_ this      · simp [closure_Ioo hR₁.2.ne, hR₁.2.le]      · apply continuousWithinAt_const      · apply ContinuousWithinAt.fun_add ?_ continuousWithinAt_const        exact small_annulus_right hf hR₁.1 |>.enorm    simpa using! le_R1  · have (R' : ℝ) (hR' : R' ∈ Ioo (dist x' x) R₁) : ‖∫ (y : X) in ball x' R₂ \ ball x' R₁, K x' y * f y‖ₑ ≤        ‖∫ (y : X) in Annulus.oo x' R' R₁, K x' y * f y‖ₑ + nontangentialOperator K f x := by      have hR'pos : 0 < R' := by linarith [dist_nonneg (x := x') (y := x), hR'.1]      have : ∫ (y : X) in Annulus.co x' R₁ R₂, K x' y * f y = (∫ (y : X) in Annulus.oo x' R' R₁, K x' y * f y) +          (∫ (y : X) in Annulus.co x' R₁ R₂, K x' y * f y) - ∫ (y : X) in Annulus.oo x' R' R₁, K x' y * f y := by        simp      rw [sdiff_eq_compl_inter, inter_comm, ← Annulus.co_eq, this]      have : Annulus.oo x' R' R₂ = Annulus.oo x' R' R₁ ∪ Annulus.co x' R₁ R₂ :=        Annulus.oo_union_co hR'.2 hR₁.2.le |>.symm      rw [← setIntegral_union_2 (disjoint_left.mpr <| fun x hx hx2 ↦ not_lt.mpr hx2.1 hx.2) (by measurability), ← this]; swap      · simp_rw [← this]        apply IntegrableOn.mono_set <| czOperator_welldefined hf hR'pos x'        rw [← Annulus.ci_eq]        exact Annulus.oo_subset_ci (by rfl)      apply le_trans enorm_sub_le      rw [add_comm]      gcongr      refine le_iSup₂_of_le ?_ (i := R₂) (j := R')      refine le_iSup₂_of_le ?_ (i := ⟨hR'pos, hR'.2.trans hR₁.2⟩) (j := x')      refine le_iSup_of_le ?_ (i := hR'.1)      rfl    -- apply continuity    have le_R1 : ‖∫ (y : X) in ball x' R₂ \ ball x' R₁, K x' y * f y‖ₑ ≤        ‖∫ (y : X) in Annulus.oo x' R₁ R₁, K x' y * f y‖ₑ + nontangentialOperator K f x := by      refine ContinuousWithinAt.closure_le ?_ ?_ ?_ this      · simp [closure_Ioo (mem_ball.mp hx').ne, (mem_ball.mp hx').le]      · apply continuousWithinAt_const      · apply ContinuousWithinAt.fun_add ?_ continuousWithinAt_const        exact small_annulus_left hf (dist_nonneg) |>.enorm    simpa using! le_R1