NontangentialOperator.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 981 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Pinned Carleson blueprint

23 declarations, 0 contain sorry, 0 declared as axioms

Section 10.1 and Lemma 10.0.2

Imports (2)

Imported by 2 files

def simpleNontangentialOperator The operator T_*^r g(x), defined in (10.1.31), above Lemma 10.1.6 line 23 source
Source documentation
The operator T_*^r g(x), defined in (10.1.31), above Lemma 10.1.6.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, MetricSpace, MeasureTheory.DoublingMeasure, NNReal, defaultA, Complex, Real, ENNReal
Proof uses: iSup, GT.gt, Membership.mem, Set, Metric.ball, ENorm.enorm, czOperator
36 instances, coercions and auxiliary constants left out.
```
def simpleNontangentialOperator (r : ℝ) (g : X → ℂ) (x : X) : ℝ≥0∞ :=
…
```
Mentions: g
lemma _laverage_mul_measure_ball line 30 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, MetricSpace, MeasureTheory.DoublingMeasure, NNReal, defaultA, Real, Complex, Eq, ENNReal, MeasureTheory.lintegral, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, Metric.ball, HMul.hMul, ENorm.enorm, MeasureTheory.laverage, MeasureTheory.Measure, Set
Proof uses: MeasureTheory.IsFiniteMeasure, Iff.mpr, Ne, Top.top, MeasureTheory.isFiniteMeasure_restrict, LT.lt.ne, MeasureTheory.measure_ball_lt_top, Eq.mpr, Set.univ, id, congrArg, Eq.symm, MeasureTheory.measure_mul_laverage, of_eq_true, Eq.trans, True, congr, Inter.inter, congrFun', mul_comm and 4 more
82 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma estimate_10_1_2 line 37 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, MetricSpace, MeasureTheory.DoublingMeasure, NNReal, defaultA, Real, Complex, IsTwoSidedKernel, BoundedFiniteSupport, MeasureTheory.MeasureSpace.volume, LT.lt, OfNat.ofNat, LE.le, ENNReal, MeasureTheory.lintegral, MeasureTheory.Measure.restrict, Inter.inter, Set, Compl.compl, Metric.ball and 5 more
Proof uses: Eq.mpr, id, Eq, congrFun', congrArg, funext, enorm_mul, Trans.simple, HDiv.hDiv, C_K, MeasureTheory.Measure, MeasureTheory.setLIntegral_mono_ae, AEMeasurable.const_mul, MeasureTheory.AEStronglyMeasurable.enorm, BoundedFiniteSupport.aestronglyMeasurable_restrict, Filter.Eventually.of_forall, Membership.mem, MeasureTheory.ae, mul_le_mul', enorm_K_le_ball_complement and 61 more
200 instances, coercions and auxiliary constants left out.

Tactic trace: 37 steps
Open to load the checked before-and-after goal states.
lemma estimate_10_1_3 line 72 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, MetricSpace, MeasureTheory.DoublingMeasure, NNReal, defaultA, Real, Complex, IsTwoSidedKernel, LE.le, OfNat.ofNat, BoundedFiniteSupport, MeasureTheory.MeasureSpace.volume, LT.lt, Dist.dist, ENNReal, ENorm.enorm, MeasureTheory.integral, MeasureTheory.Measure.restrict, Compl.compl, Set and 6 more
Proof uses: Eq.mpr, id, Eq, congrFun', congrArg, funext, Trans.simple, MeasureTheory.lintegral, MeasureTheory.enorm_integral_le_lintegral_enorm, enorm_mul, HDiv.hDiv, EDist.edist, Inv.inv, C_K, vol, MeasureTheory.setLIntegral_mono_ae, AEMeasurable.fun_mul, AEMeasurable.pow_const, AEMeasurable.const_div, MeasureTheory.AEStronglyMeasurable.edist and 202 more
362 instances, coercions and auxiliary constants left out.

Tactic trace: 165 steps
Open to load the checked before-and-after goal states.
lemma estimate_10_1_4 line 197 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, MetricSpace, MeasureTheory.DoublingMeasure, NNReal, defaultA, Real, Complex, IsTwoSidedKernel, BoundedFiniteSupport, MeasureTheory.MeasureSpace.volume, LT.lt, OfNat.ofNat, LE.le, Dist.dist, ENNReal, MeasureTheory.lintegral, MeasureTheory.Measure.restrict, Inter.inter, Set, Compl.compl and 6 more
Proof uses: Eq.mpr, id, Eq, congrFun', congrArg, funext, enorm_mul, Trans.simple, HDiv.hDiv, C_K, MeasureTheory.Measure, MeasureTheory.setLIntegral_mono_ae, AEMeasurable.const_mul, MeasureTheory.AEStronglyMeasurable.enorm, BoundedFiniteSupport.aestronglyMeasurable_restrict, Filter.Eventually.of_forall, Membership.mem, MeasureTheory.ae, mul_le_mul', enorm_K_le_ball_complement and 101 more
225 instances, coercions and auxiliary constants left out.

Tactic trace: 41 steps
Open to load the checked before-and-after goal states.
theorem estimate_x_shift Lemma 10.1.2 line 233 source
Source documentation
Lemma 10.1.2

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, MetricSpace, MeasureTheory.DoublingMeasure, NNReal, defaultA, Real, Complex, IsTwoSidedKernel, LE.le, OfNat.ofNat, BoundedFiniteSupport, MeasureTheory.MeasureSpace.volume, LT.lt, Dist.dist, ENNReal, EDist.edist, czOperator, HMul.hMul, C10_1_2, globalMaximalFunction
Proof uses: Set, Compl.compl, Metric.ball, Eq, Union.union, Inter.inter, Eq.mpr, id, Eq.rec, Eq.refl, Eq.trans, Set.univ, congrArg, Eq.symm, Set.inter_univ, Set.union_compl_self, Set.inter_union_distrib_left, Union, propext, Set.right_eq_inter and 129 more
257 instances, coercions and auxiliary constants left out.

Tactic trace: 78 steps
Open to load the checked before-and-after goal states.
```
theorem estimate_x_shift (ha : 4 ≤ a)
    {g : X → ℂ} (hg : BoundedFiniteSupport g) (hr : 0 < r) (hx : dist x x' ≤ r) :
    edist (czOperator K r g x) (czOperator K r g x') ≤
    C10_1_2 a * globalMaximalFunction volume 1 g x := by
…
```
Mentions: g, BoundedFiniteSupport, czOperator, K
lemma radius_change line 323 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, MetricSpace, MeasureTheory.DoublingMeasure, NNReal, defaultA, Real, Complex, IsTwoSidedKernel, BoundedFiniteSupport, MeasureTheory.MeasureSpace.volume, Membership.mem, Set, Set.Ioc, OfNat.ofNat, LE.le, Dist.dist, HDiv.hDiv, ENNReal, ENorm.enorm, HSub.hSub and 8 more
Proof uses: LT.lt, lt_of_not_ge, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.cast_zero, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_zero, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.mpr, Eq and 195 more
315 instances, coercions and auxiliary constants left out.

Tactic trace: 133 steps
Open to load the checked before-and-after goal states.
lemma cut_out_ball line 448 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, MetricSpace, MeasureTheory.DoublingMeasure, NNReal, defaultA, Real, Complex, Membership.mem, Set, Set.Ioc, OfNat.ofNat, LE.le, Dist.dist, HDiv.hDiv, Eq, czOperator, Set.indicator, Compl.compl, Metric.ball
Proof uses: LT.lt, lt_of_not_ge, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HAdd.hAdd, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HMul.hMul, HPow.hPow, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.cast_zero, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_zero and 88 more
132 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
theorem cotlar_control Lemma 10.1.3 line 468 source
Source documentation
Lemma 10.1.3

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, MetricSpace, MeasureTheory.DoublingMeasure, NNReal, defaultA, Real, Complex, IsTwoSidedKernel, LE.le, OfNat.ofNat, BoundedFiniteSupport, MeasureTheory.MeasureSpace.volume, Membership.mem, Set, Set.Ioc, Dist.dist, HDiv.hDiv, ENNReal, ENorm.enorm, czOperator and 7 more
Proof uses: LT.lt, lt_of_not_ge, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HPow.hPow, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.cast_zero, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_zero, Mathlib.Tactic.Ring.Common.atom_pf, rfl and 109 more
245 instances, coercions and auxiliary constants left out.

Tactic trace: 34 steps
Open to load the checked before-and-after goal states.
```
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
…
```
Mentions: g, BoundedFiniteSupport, czOperator, K
lemma globalMaximalFunction_zero_enorm_ae_zero line 517 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, MetricSpace, MeasureTheory.DoublingMeasure, NNReal, defaultA, Real, LT.lt, OfNat.ofNat, Complex, MeasureTheory.AEStronglyMeasurable, MeasureTheory.MeasureSpace.volume, Eq, ENNReal, globalMaximalFunction, Filter.Eventually, ENorm.enorm, MeasureTheory.ae, MeasureTheory.Measure, MeasureTheory.Measure.restrict, Metric.ball
Proof uses: id, Eq.mpr, Filter.EventuallyEq, MeasureTheory.lintegral, congrArg, Eq.symm, propext, MeasureTheory.lintegral_eq_zero_iff', MeasureTheory.AEStronglyMeasurable.enorm, MeasureTheory.AEStronglyMeasurable.restrict, Bot.bot, ENNReal.bot_eq_zero, LE.le, le_bot_iff, le_of_le_of_eq, HMul.hMul, Set, lintegral_ball_le_volume_mul_globalMaximalFunction, of_eq_true, Dist.dist and 7 more
90 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
theorem cotlar_set_F₁ Part 1 of Lemma 10.1.4 about F₁ line 529 source
Source documentation
Part 1 of Lemma 10.1.4 about F₁.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, MetricSpace, MeasureTheory.DoublingMeasure, NNReal, defaultA, Real, Complex, IsTwoSidedKernel, LT.lt, OfNat.ofNat, LE.le, BoundedFiniteSupport, MeasureTheory.MeasureSpace.volume, ENNReal, MeasureTheory.Measure, Set, MeasureTheory.Measure.restrict, Metric.ball, HDiv.hDiv, Set.ofPred and 4 more
Proof uses: dite, Eq, le_of_eq_of_le, Eq.mpr, Filter.Eventually, Not, Membership.mem, MeasureTheory.ae, id, congrArg, propext, MeasureTheory.measure_eq_zero_iff_ae_notMem, globalMaximalFunction_zero_enorm_ae_zero, of_eq_true, Eq.trans, True, lt_of_lt_of_le, czOperator_aestronglyMeasurable_aux, Filter.mp_mem, Filter.univ_mem' and 46 more
189 instances, coercions and auxiliary constants left out.

Tactic trace: 45 steps
Open to load the checked before-and-after goal states.
```
theorem cotlar_set_F₁ (hr : 0 < r) (hR : r ≤ R) {g : X → ℂ} (hg : BoundedFiniteSupport g) :
    volume.restrict (ball x (R / 4))
      {x' | 4 * globalMaximalFunction volume 1 (czOperator K r g) x < ‖czOperator K r g x'‖ₑ } ≤
    volume (ball x (R / 4)) / 4 := by
…
```
Mentions: g, BoundedFiniteSupport, czOperator, K
theorem cotlar_set_F₂ Part 2 of Lemma 10.1.4 about F₂ line 568 source
Source documentation
Part 2 of Lemma 10.1.4 about F₂.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, MetricSpace, MeasureTheory.DoublingMeasure, NNReal, defaultA, Real, Complex, IsTwoSidedKernel, LE.le, OfNat.ofNat, LT.lt, GT.gt, MeasureTheory.HasBoundedStrongType, czOperator, ENNReal, MeasureTheory.MeasureSpace.volume, C_Ts, BoundedFiniteSupport, MeasureTheory.Measure, Set and 9 more
Proof uses: dite, Eq, le_of_eq_of_le, Eq.mpr, Filter.Eventually, Not, Membership.mem, MeasureTheory.ae, id, congrArg, propext, MeasureTheory.measure_eq_zero_iff_ae_notMem, globalMaximalFunction_zero_enorm_ae_zero, of_eq_true, Eq.trans, True, lt_of_lt_of_le, BoundedFiniteSupport.aestronglyMeasurable, Bot.bot, congrFun' and 173 more
318 instances, coercions and auxiliary constants left out.

Tactic trace: 81 steps
Open to load the checked before-and-after goal states.
```
theorem cotlar_set_F₂ (ha : 4 ≤ a) (hr : 0 < r) (hR : r ≤ R)
    (hT : ∀ r > 0, HasBoundedStrongType (czOperator K r) 2 2 volume volume (C_Ts a))
    {g : X → ℂ} (hg : BoundedFiniteSupport g) :
    volume.restrict (ball x (R / 4))
      {x' | C10_1_4 a * globalMaximalFunction volume 1 g x <
        ‖czOperator K r ((ball x (R / 2)).indicator g) x'‖ₑ } ≤
    volume (ball x (R / 4)) / 4 := by
…
```
Mentions: czOperator, K, C_Ts, g, BoundedFiniteSupport
theorem cotlar_estimate Lemma 10.1.5 line 646 source
Source documentation
Lemma 10.1.5

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, MetricSpace, MeasureTheory.DoublingMeasure, NNReal, defaultA, Real, Complex, IsTwoSidedKernel, LE.le, OfNat.ofNat, GT.gt, MeasureTheory.HasBoundedStrongType, czOperator, ENNReal, MeasureTheory.MeasureSpace.volume, C_Ts, BoundedFiniteSupport, Membership.mem, Set, Set.Ioc and 5 more
Proof uses: Set.ofPred, LT.lt, C10_1_4, Set.indicator, Metric.ball, HDiv.hDiv, Inter.inter, Compl.compl, Union.union, MeasureTheory.Measure, MeasureTheory.Measure.restrict, le_trans, MeasureTheory.measure_union_le, cotlar_set_F₁, And.left, And.right, cotlar_set_F₂, id, le_of_le_of_eq, add_le_add and 136 more
231 instances, coercions and auxiliary constants left out.

Tactic trace: 59 steps
Open to load the checked before-and-after goal states.
```
theorem cotlar_estimate (ha : 4 ≤ a)
    (hT : ∀ r > 0, HasBoundedStrongType (czOperator K r) 2 2 volume volume (C_Ts a))
    {g : X → ℂ} (hg : BoundedFiniteSupport g) (hr : r ∈ Ioc 0 R) :
    ‖czOperator K R g x‖ₑ ≤ 4 * globalMaximalFunction volume 1 (czOperator K r g) x +
      C10_1_5 a * globalMaximalFunction volume 1 g x := by
…
```
Mentions: czOperator, K, C_Ts, g, BoundedFiniteSupport
lemma lowerSemicontinuous_simpleNontangentialOperator Part of Lemma 10.1.6 line 701 source
Source documentation
Part of Lemma 10.1.6.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, MetricSpace, MeasureTheory.DoublingMeasure, NNReal, defaultA, Real, Complex, LowerSemicontinuous, ENNReal, simpleNontangentialOperator
Proof uses: id, Eq.mpr, iSup, GT.gt, Membership.mem, Set, Metric.ball, ENorm.enorm, czOperator, IsOpen, Set.preimage, Set.Ioi, Eq, Set.ofPred, LT.lt, forall_congr, congrArg, funext, Exists, Eq.trans and 20 more
61 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
```
lemma lowerSemicontinuous_simpleNontangentialOperator {g : X → ℂ} :
    LowerSemicontinuous (simpleNontangentialOperator K r g) := by
…
```
Mentions: g, simpleNontangentialOperator, K
lemma aestronglyMeasurable_simpleNontangentialOperator line 715 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, MetricSpace, MeasureTheory.DoublingMeasure, NNReal, defaultA, Real, Complex, MeasureTheory.AEStronglyMeasurable, ENNReal, simpleNontangentialOperator, MeasureTheory.MeasureSpace.volume
Proof uses: Measurable.aestronglyMeasurable, LowerSemicontinuous.measurable, lowerSemicontinuous_simpleNontangentialOperator
31 instances, coercions and auxiliary constants left out.
theorem simple_nontangential_operator Lemma 10.1.6 line 725 source
Source documentation
Lemma 10.1.6. The formal statement includes the measurability of the operator. See also simple_nontangential_operator_le

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, MetricSpace, MeasureTheory.DoublingMeasure, NNReal, defaultA, Real, Complex, IsTwoSidedKernel, LE.le, OfNat.ofNat, GT.gt, MeasureTheory.HasBoundedStrongType, czOperator, ENNReal, MeasureTheory.MeasureSpace.volume, C_Ts, LT.lt, simpleNontangentialOperator, C10_1_6
Proof uses: BoundedFiniteSupport, And.intro, MeasureTheory.AEStronglyMeasurable, MeasureTheory.eLpNorm, HMul.hMul, aestronglyMeasurable_simpleNontangentialOperator, HAdd.hAdd, globalMaximalFunction, HSMul.hSMul, C10_1_5, C10_1_2, Trans.simple, MeasureTheory.eLpNorm_mono_enorm, id, ENorm.enorm, Eq.mpr, iSup, Membership.mem, Set, Metric.ball and 185 more
341 instances, coercions and auxiliary constants left out.

Tactic trace: 79 steps
Open to load the checked before-and-after goal states.
```
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
…
```
Mentions: czOperator, K, C_Ts, simpleNontangentialOperator
theorem simple_nontangential_operator_le This is the first step of the proof of Lemma 10.0.2, and should follow from 10.1.6 + monotone convergence theorem line 796 source
Source documentation
This is the first step of the proof of Lemma 10.0.2, and should follow from 10.1.6 + monotone convergence theorem. (measurability should be proven without any restriction on r.)

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, MetricSpace, MeasureTheory.DoublingMeasure, NNReal, defaultA, Real, Complex, IsTwoSidedKernel, LE.le, OfNat.ofNat, GT.gt, MeasureTheory.HasBoundedStrongType, czOperator, ENNReal, MeasureTheory.MeasureSpace.volume, C_Ts, simpleNontangentialOperator, C10_1_6
Proof uses: dite, LT.lt, simple_nontangential_operator, Not, Eq, Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt, Not.intro, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HAdd.hAdd, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HMul.hMul, HPow.hPow, Nat.rawCast, Int.rawCast, inferInstance, Ring and 105 more
194 instances, coercions and auxiliary constants left out.

Tactic trace: 49 steps
Open to load the checked before-and-after goal states.
```
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
…
```
Mentions: czOperator, K, C_Ts, simpleNontangentialOperator
theorem small_annulus_right Part of Lemma 10.1.7, reformulated line 837 source
Source documentation
Part of Lemma 10.1.7, reformulated.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, MetricSpace, MeasureTheory.DoublingMeasure, NNReal, defaultA, Complex, IsTwoSidedKernel, BoundedFiniteSupport, MeasureTheory.MeasureSpace.volume, Real, LT.lt, OfNat.ofNat, ContinuousWithinAt, MeasureTheory.integral, MeasureTheory.Measure.restrict, Set.Annulus.oo, HMul.hMul, Set.Ioo
Proof uses: dite, Eq.mpr, Set.indicator, id, Eq, Eq.rec, Set, Eq.refl, funext, Eq.trans, congrArg, Eq.symm, MeasureTheory.integral_indicator, Set.Annulus.measurableSet_oo, Filter.Eventually, LE.le, Norm.norm, MeasureTheory.ae, MeasureTheory.Measure, Compl.compl and 126 more
203 instances, coercions and auxiliary constants left out.

Tactic trace: 73 steps
Open to load the checked before-and-after goal states.
```
theorem small_annulus_right {g : X → ℂ} (hg : BoundedFiniteSupport g) {R₁ R₂ : ℝ} (hR₁ : 0 < R₁) :
    ContinuousWithinAt (fun R₂ ↦ ∫ y in Annulus.oo x R₁ R₂, K x y * g y) (Ioo R₁ R₂) R₁ := by
…
```
Mentions: g, BoundedFiniteSupport, K
theorem small_annulus_left Part of Lemma 10.1.7, reformulated line 894 source
Source documentation
Part of Lemma 10.1.7, reformulated

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, MetricSpace, MeasureTheory.DoublingMeasure, NNReal, defaultA, Complex, IsTwoSidedKernel, BoundedFiniteSupport, MeasureTheory.MeasureSpace.volume, Real, LE.le, OfNat.ofNat, ContinuousWithinAt, MeasureTheory.integral, MeasureTheory.Measure.restrict, Set.Annulus.oo, HMul.hMul, Set.Ioo
Proof uses: dite, LT.lt, Eq.mpr, Set.indicator, id, Eq, Eq.rec, Set, Eq.refl, funext, Eq.trans, congrArg, Eq.symm, MeasureTheory.integral_indicator, Set.Annulus.measurableSet_oo, Filter.Eventually, Norm.norm, MeasureTheory.ae, MeasureTheory.Measure, Compl.compl and 161 more
237 instances, coercions and auxiliary constants left out.

Tactic trace: 74 steps
Open to load the checked before-and-after goal states.
```
theorem small_annulus_left {g : X → ℂ} (hg : BoundedFiniteSupport g) {R₁ R₂ : ℝ} (hR₁ : 0 ≤ R₁) :
    ContinuousWithinAt (fun R ↦ ∫ y in Annulus.oo x R R₂, K x y * g y) (Ioo R₁ R₂) R₂ := by
…
```
Mentions: g, BoundedFiniteSupport, K
theorem nontangential_operator_boundary Lemma 10.1.8 line 951 source
Source documentation
Lemma 10.1.8.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, MetricSpace, MeasureTheory.DoublingMeasure, NNReal, defaultA, Complex, IsTwoSidedKernel, BoundedFiniteSupport, MeasureTheory.MeasureSpace.volume, Eq, ENNReal, nontangentialOperator, iSup, Real, Membership.mem, Set, Set.Ioo, OfNat.ofNat, Metric.ball, ENorm.enorm and 4 more
Proof uses: id, le_antisymm, Set.Annulus.oo, Eq.mpr, LE.le, congrArg, propext, iSup_le_iff, iSup₂_le_iff, HAdd.hAdd, Union.union, Set.Annulus.co, Eq.symm, Set.Annulus.oo_union_co, And.left, LT.lt, LT.lt.le, And.right, MeasureTheory.setIntegral_union_2, Iff.mpr and 105 more
206 instances, coercions and auxiliary constants left out.

Tactic trace: 74 steps
Open to load the checked before-and-after goal states.
```
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
…
```
Mentions: BoundedFiniteSupport, nontangentialOperator, K
lemma lowerSemicontinuous_nontangentialOperator Part of Lemma 10.1.6 line 1023 source
Source documentation
Part of Lemma 10.1.6.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, MetricSpace, MeasureTheory.DoublingMeasure, NNReal, defaultA, Complex, LowerSemicontinuous, ENNReal, nontangentialOperator
Proof uses: id, Eq.mpr, iSup, Real, Membership.mem, Set, Set.Ioo, OfNat.ofNat, Metric.ball, ENorm.enorm, MeasureTheory.integral, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, Set.Annulus.oo, HMul.hMul, IsOpen, Set.preimage, Set.Ioi, Eq, Set.ofPred and 27 more
72 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
```
lemma lowerSemicontinuous_nontangentialOperator {g : X → ℂ} :
    LowerSemicontinuous (nontangentialOperator K g) := by
…
```
Mentions: g, nontangentialOperator, K
lemma aestronglyMeasurable_nontangentialOperator line 1037 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, MetricSpace, MeasureTheory.DoublingMeasure, NNReal, defaultA, Complex, MeasureTheory.AEStronglyMeasurable, ENNReal, nontangentialOperator, MeasureTheory.MeasureSpace.volume
Proof uses: Measurable.aestronglyMeasurable, LowerSemicontinuous.measurable, lowerSemicontinuous_nontangentialOperator
31 instances, coercions and auxiliary constants left out.
theorem nontangential_from_simple Lemma 10.0.2 line 1045 source
Source documentation
Lemma 10.0.2. The formal statement includes the measurability of the operator.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, MetricSpace, MeasureTheory.DoublingMeasure, NNReal, defaultA, Complex, IsTwoSidedKernel, LE.le, OfNat.ofNat, Real, GT.gt, MeasureTheory.HasBoundedStrongType, czOperator, ENNReal, MeasureTheory.MeasureSpace.volume, C_Ts, nontangentialOperator, C10_0_2
Proof uses: BoundedFiniteSupport, MeasureTheory.eLpNorm, simpleNontangentialOperator, HMul.hMul, C10_1_6, And.right, MeasureTheory.AEStronglyMeasurable, simple_nontangential_operator_le, le_rfl, And.intro, aestronglyMeasurable_nontangentialOperator, Trans.simple, id, Eq.mpr, HAdd.hAdd, Eq, congrArg, two_mul, add_mul, le_trans and 104 more
199 instances, coercions and auxiliary constants left out.

Tactic trace: 55 steps
Open to load the checked before-and-after goal states.
```
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
…
```
Mentions: czOperator, K, C_Ts, nontangentialOperator