PointwiseEstimate.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

70 declarations, 0 contain sorry, 0 declared as axioms

Section 7.1 and Lemma 7.1.3

Imports (3)

Imported by 2 files

def TileStructure.Forest.σ The definition σ(u, x) given in Section 7.1 line 29 source
Source documentation
The definition σ(u, x) given in Section 7.1. We may assume u ∈ t whenever proving things about this definition.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, TileStructure.Forest, 𝔓, Finset
Proof uses: Finset.image, 𝔰, Finset.filter, And, Membership.mem, TileStructure.Forest.𝔗, E, Classical.propDecidable, Finset.univ
30 instances, coercions and auxiliary constants left out.
```
def σ (u : 𝔓 X) (x : X) : Finset ℤ := .image 𝔰 { p | p ∈ t u ∧ x ∈ E p }
…
```
Mentions: 𝔓, 𝔰, E
lemma TileStructure.Forest.exists_p_of_mem_σ line 32 source
def TileStructure.Forest.σMax line 40 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, TileStructure.Forest, 𝔓, Finset.Nonempty, TileStructure.Forest.σ
Proof uses: Finset.max'
27 instances, coercions and auxiliary constants left out.
def TileStructure.Forest.σMin line 45 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, TileStructure.Forest, 𝔓, Finset.Nonempty, TileStructure.Forest.σ
Proof uses: Finset.min'
27 instances, coercions and auxiliary constants left out.
lemma TileStructure.Forest.σMax_mem_σ line 49 source
def TileStructure.Forest.𝓙₀ The definition of `𝓙₀(𝔖), defined above Lemma 7.1.2 line 53 source
Source documentation
The definition of `𝓙₀(𝔖), defined above Lemma 7.1.2

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, Grid
Proof uses: Set.ofPred, Or, Eq, s, Neg.neg, Membership.mem, Not, LE.le, 𝓘, Metric.ball, c, HMul.hMul, OfNat.ofNat, HPow.hPow, HAdd.hAdd
45 instances, coercions and auxiliary constants left out.
```
def 𝓙₀ (𝔖 : Set (𝔓 X)) : Set (Grid X) :=
…
```
Mentions: 𝔓, Grid
def TileStructure.Forest.𝓙 The definition of `𝓙(𝔖), defined above Lemma 7.1.2 line 57 source
Source documentation
The definition of `𝓙(𝔖), defined above Lemma 7.1.2

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, Grid
Proof uses: Set.ofPred, Maximal, Membership.mem, TileStructure.Forest.𝓙₀
32 instances, coercions and auxiliary constants left out.
```
def 𝓙 (𝔖 : Set (𝔓 X)) : Set (Grid X) :=
…
```
Mentions: 𝔓, Grid
lemma TileStructure.Forest.𝓙_subset_𝓙₀ line 60 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, LE.le, Grid, TileStructure.Forest.𝓙, TileStructure.Forest.𝓙₀
Proof uses: Set.sep_subset, Membership.mem
33 instances, coercions and auxiliary constants left out.
lemma TileStructure.Forest.pairwiseDisjoint_𝓙 line 62 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, Set.PairwiseDisjoint, Grid, TileStructure.Forest.𝓙
Proof uses: Membership.mem, Ne, IsAntichain, LE.le, setOfPred_maximal_antichain, TileStructure.Forest.𝓙₀, Or.resolve_left, Disjoint, Or, le_or_ge_or_disjoint, Ne.symm
52 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma TileStructure.Forest.S_eq_zero_of_topCube_mem_𝓙₀ line 66 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, Set.Nonempty, Membership.mem, GridStructure.Grid, Grid and 4 more
Proof uses: Neg.neg, Or.resolve_right, Not, LE.le, 𝓘, Metric.ball, c, HMul.hMul, HPow.hPow, HAdd.hAdd, Eq.mp, Or, GridStructure.s, congrArg, GridStructure.s_topCube, s, s.eq_1, Set.ofPred, Set.mem_ofPred_eq, TileStructure.Forest.𝓙₀.eq_1 and 36 more
110 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
def TileStructure.Forest.𝓛₀ The definition of `𝓛₀(𝔖), defined above Lemma 7.1.2 line 80 source
Source documentation
The definition of `𝓛₀(𝔖), defined above Lemma 7.1.2

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, Grid
Proof uses: Set.ofPred, Or, Eq, s, Neg.neg, And, Exists, Membership.mem, LE.le, 𝓘, Not
34 instances, coercions and auxiliary constants left out.
```
def 𝓛₀ (𝔖 : Set (𝔓 X)) : Set (Grid X) :=
…
```
Mentions: 𝔓, Grid
def TileStructure.Forest.𝓛 The definition of `𝓛(𝔖), defined above Lemma 7.1.2 line 84 source
Source documentation
The definition of `𝓛(𝔖), defined above Lemma 7.1.2

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, Grid
Proof uses: Set.ofPred, Maximal, Membership.mem, TileStructure.Forest.𝓛₀
32 instances, coercions and auxiliary constants left out.
```
def 𝓛 (𝔖 : Set (𝔓 X)) : Set (Grid X) :=
…
```
Mentions: 𝔓, Grid
lemma TileStructure.Forest.𝓛_subset_𝓛₀ line 87 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, LE.le, Grid, TileStructure.Forest.𝓛, TileStructure.Forest.𝓛₀
Proof uses: Set.sep_subset, Membership.mem
33 instances, coercions and auxiliary constants left out.
lemma TileStructure.Forest.s_le_s_of_mem_𝓛 line 89 source
lemma TileStructure.Forest.subset_of_mem_𝓛 line 97 source
lemma TileStructure.Forest.le_of_mem_𝓛 line 101 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, Grid, Membership.mem, TileStructure.Forest.𝓛, Not and 3 more
Proof uses: And.intro, Prod.fst, GridStructure.Grid, Prod.mk, GridStructure.s, Prod.snd
62 instances, coercions and auxiliary constants left out.
def TileStructure.Forest.approxOnCube The projection operator P_𝓒 f(x), given above Lemma 7.1.3 line 108 source
Source documentation
The projection operator P_𝓒 f(x), given above Lemma 7.1.3. In lemmas the c will be pairwise disjoint on C.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, NormedAddCommGroup, NormedSpace, Grid
Proof uses: Finset.sum, Finset.filter, Membership.mem, Classical.propDecidable, Finset.univ, Set.indicator, MeasureTheory.average, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume
44 instances, coercions and auxiliary constants left out.
```
def approxOnCube (C : Set (Grid X)) (f : X → E') (x : X) : E' :=
…
```
Mentions: Grid
lemma TileStructure.Forest.stronglyMeasurable_approxOnCube line 111 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, NormedAddCommGroup, NormedSpace, Grid, MeasureTheory.StronglyMeasurable, TileStructure.Forest.approxOnCube
Proof uses: Finset.stronglyMeasurable_fun_sum, Set.indicator, MeasureTheory.average, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, Finset.filter, Membership.mem, Classical.propDecidable, Finset.univ, Finset, MeasureTheory.StronglyMeasurable.indicator, MeasureTheory.stronglyMeasurable_const, GridStructure.coeGrid_measurable
57 instances, coercions and auxiliary constants left out.
lemma TileStructure.Forest.integrable_approxOnCube line 116 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, NormedAddCommGroup, NormedSpace, Grid, MeasureTheory.Integrable, TileStructure.Forest.approxOnCube and 1 more
Proof uses: MeasureTheory.integrable_finsetSum, Finset.filter, Membership.mem, Classical.propDecidable, Finset.univ, Set.indicator, MeasureTheory.average, MeasureTheory.Measure.restrict, Finset, And.intro, MeasureTheory.AEStronglyMeasurable, MeasureTheory.HasFiniteIntegral, Iff.mpr, aestronglyMeasurable_indicator_iff, GridStructure.coeGrid_measurable, MeasureTheory.aestronglyMeasurable_const, Eq.mpr, LT.lt, ENNReal, MeasureTheory.lintegral and 16 more
83 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma TileStructure.Forest.approxOnCube_nonneg line 124 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, Grid, GE.ge, OfNat.ofNat, TileStructure.Forest.approxOnCube
Proof uses: Finset.sum_nonneg', Set.indicator, MeasureTheory.average, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, Finset.filter, Membership.mem, Classical.propDecidable, Finset.univ, Set.indicator_nonneg, MeasureTheory.integral, HSMul.hSMul, ENNReal, MeasureTheory.Measure, Inv.inv, Set.univ, MeasureTheory.integral_nonneg
88 instances, coercions and auxiliary constants left out.
lemma TileStructure.Forest.approxOnCube_apply line 129 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, NormedAddCommGroup, NormedSpace, Grid, Set.PairwiseDisjoint, Membership.mem and 5 more
Proof uses: Eq.mpr, Finset.sum, Finset.filter, Classical.propDecidable, Finset.univ, Set.indicator, id, congrArg, TileStructure.Forest.approxOnCube.eq_1, HAdd.hAdd, Not, Eq.symm, Finset.sum_filter_not_add_sum_filter, OfNat.ofNat, Finset, Set.indicator_of_notMem, Iff.mp, Disjoint, Set.disjoint_left, Or.resolve_left and 20 more
92 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
lemma TileStructure.Forest.boundedCompactSupport_approxOnCube line 150 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, RCLike, Grid, MeasureTheory.BoundedCompactSupport, TileStructure.Forest.approxOnCube, MeasureTheory.MeasureSpace.volume
Proof uses: MeasureTheory.BoundedCompactSupport.finset_sum, Finset.filter, Membership.mem, Classical.propDecidable, Finset.univ, Set.indicator, MeasureTheory.average, MeasureTheory.Measure.restrict, Finset, MeasureTheory.BoundedCompactSupport.indicator_of_isCompact_closure, MeasureTheory.memLp_top_const, Bornology.IsBounded.isCompact_closure, Iff.mpr, Bornology.IsBounded, Exists, LE.le, Metric.ball, c, Metric.isBounded_iff_subset_ball, Exists.intro and 6 more
100 instances, coercions and auxiliary constants left out.
lemma TileStructure.Forest.lintegral_eq_lintegral_approxOnCube Used in the proof of Lemma 7.1.6 line 158 source
Source comment
Used in the proof of Lemma 7.1.6

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, Grid, Set.PairwiseDisjoint, Membership.mem, MeasureTheory.BoundedCompactSupport, MeasureTheory.MeasureSpace.volume and 7 more
Proof uses: Filter.EventuallyLE, MeasureTheory.ae, MeasureTheory.Measure, OfNat.ofNat, Filter.Eventually.of_forall, LE.le, of_eq_true, Eq.trans, True, forall_congr, implies_true, Ne, Ne.symm, LT.lt.ne, volume_coeGrid_pos, defaultD_pos, ENNReal.ofReal, MeasureTheory.average, MeasureTheory.setLIntegral_congr_fun, GridStructure.coeGrid_measurable and 69 more
235 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
```
lemma lintegral_eq_lintegral_approxOnCube {C : Set (Grid X)}
    (hC : C.PairwiseDisjoint fun I ↦ (I : Set X)) {J : Grid X} (hJ : J ∈ C) {f : X → ℂ}
    (hf : BoundedCompactSupport f) :
    ∫⁻ y in J, ‖f y‖ₑ = ∫⁻ y in J, ‖approxOnCube C (fun x ↦ (‖f x‖ : ℂ)) y‖ₑ := by
…
```
Mentions: Grid, TileStructure.Forest.approxOnCube
lemma TileStructure.Forest.approxOnCube_ofReal line 187 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, Grid, Eq, TileStructure.Forest.approxOnCube
Proof uses: Eq.mpr, Finset.sum, Finset.filter, Membership.mem, Classical.propDecidable, Finset.univ, Set.indicator, MeasureTheory.average, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, id, congrFun', congrArg, Finset.sum_congr, Eq.refl, Finset, Complex.ofReal_sum, rfl, dite, congr and 15 more
71 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma TileStructure.Forest.norm_approxOnCube_le_approxOnCube_norm line 195 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, NormedAddCommGroup, NormedSpace, Grid, LE.le, Norm.norm and 1 more
Proof uses: LE.le.trans, Finset.sum, Finset.filter, Membership.mem, Classical.propDecidable, Finset.univ, Set.indicator, MeasureTheory.average, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, norm_sum_le, Finset.sum_le_sum, Finset, Eq.mpr, id, Eq, congrArg, norm_indicator_eq_indicator_norm, Set.indicator_le_indicator, MeasureTheory.norm_integral_le_integral_norm and 5 more
78 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
def TileStructure.Forest.cubeOf The definition I_i(x), given above Lemma 7.1.3 line 204 source
Source documentation
The definition I_i(x), given above Lemma 7.1.3. The cube of scale s that contains x. There is at most 1 such cube, if it exists.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, Grid
Proof uses: Classical.epsilon, And, Membership.mem, Eq, s
30 instances, coercions and auxiliary constants left out.
```
def cubeOf (i : ℤ) (x : X) : Grid X :=
…
```
Mentions: Grid
lemma TileStructure.Forest.cubeOf_spec line 207 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, Membership.mem, Set.Icc, Neg.neg, Grid, And and 3 more
Proof uses: Classical.epsilon_spec, dite, Exists, Exists.intro, GridStructure.topCube, And.intro, GridStructure.subset_topCube, Eq.rec, GridStructure.s_topCube, Eq.symm, Not, GridStructure.Grid, Set.preimage, GridStructure.s, Singleton.singleton, Iff.mp, Set.iUnion, Set.mem_iUnion₂, GridStructure.Grid_subset_biUnion, LE.le and 8 more
54 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
def TileStructure.Forest.nontangentialMaximalFunction The definition T_𝓝^θ f(x), given in (7.1.3) line 220 source
Source documentation
The definition T_𝓝^θ f(x), given in (7.1.3). For convenience, the suprema are written a bit differently than in the blueprint (avoiding cubeOf), but this should be equivalent. This is 0 if x doesn't lie in a cube.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, FunctionDistances.Θ, ENNReal
Proof uses: iSup, Grid, Membership.mem, Set.Icc, s, LE.le, ENNReal.ofReal, HPow.hPow, HSub.hSub, OfNat.ofNat, upperRadius, MeasureTheory.SimpleFunc, ENorm.enorm, Finset.sum, Set.toFinset, MeasureTheory.integral, MeasureTheory.MeasureSpace.volume, HMul.hMul, Ks
79 instances, coercions and auxiliary constants left out.
```
def nontangentialMaximalFunction (θ : Θ X) (f : X → ℂ) (x : X) : ℝ≥0∞ :=
…
```
theorem TileStructure.Forest.MeasureTheory.Measurable.nontangentialMaximalFunction line 225 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, FunctionDistances.Θ, Measurable, ENNReal, TileStructure.Forest.nontangentialMaximalFunction
Proof uses: Measurable.iSup, Grid, iSup, Membership.mem, Set.Icc, s, LE.le, ENNReal.ofReal, HPow.hPow, HSub.hSub, OfNat.ofNat, upperRadius, MeasureTheory.SimpleFunc, ENorm.enorm, Finset.sum, Set.toFinset, MeasureTheory.integral, MeasureTheory.MeasureSpace.volume, HMul.hMul, Ks and 35 more
113 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma TileStructure.Forest.mem_𝓙_of_mem_𝓙' line 240 source
def TileStructure.Forest.ijIntegral Scaled integral appearing in the definition of boundaryOperator line 247 source
Source documentation
Scaled integral appearing in the definition of boundaryOperator.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, Grid, ENNReal
Proof uses: HMul.hMul, HDiv.hDiv, HPow.hPow, HSub.hSub, s, MeasureTheory.Measure, MeasureTheory.MeasureSpace.volume, Metric.ball, c, OfNat.ofNat, MeasureTheory.lintegral, MeasureTheory.Measure.restrict, ENorm.enorm
67 instances, coercions and auxiliary constants left out.
```
def ijIntegral : ℝ≥0∞ :=
…
```
lemma TileStructure.Forest.ijIntegral_lt_top line 250 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, Grid, MeasureTheory.BoundedCompactSupport, MeasureTheory.MeasureSpace.volume, LT.lt, ENNReal and 2 more
Proof uses: ENNReal.mul_lt_top, HDiv.hDiv, HPow.hPow, HSub.hSub, s, MeasureTheory.Measure, Metric.ball, c, HMul.hMul, OfNat.ofNat, MeasureTheory.lintegral, MeasureTheory.Measure.restrict, ENorm.enorm, ENNReal.div_lt_top, of_eq_true, Ne, Eq.trans, 𝕔, True, congrFun' and 28 more
166 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
def TileStructure.Forest.boundaryOperator The operator S_{1,𝔲} f(x), given in (7.1.4) line 257 source
Source documentation
The operator S_{1,𝔲} f(x), given in (7.1.4).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, TileStructure.Forest, 𝔓, ENNReal
Proof uses: Finset.sum, Grid, Finset.univ, Set.indicator, TileStructure.Forest.𝓙', c, s, TileStructure.Forest.ijIntegral
31 instances, coercions and auxiliary constants left out.
```
def boundaryOperator (u : 𝔓 X) (f : X → ℂ) (x : X) : ℝ≥0∞ :=
…
```
Mentions: 𝔓
lemma TileStructure.Forest.measurable_boundaryOperator line 260 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, TileStructure.Forest, 𝔓, Measurable, ENNReal, TileStructure.Forest.boundaryOperator
Proof uses: Finset.measurable_sum, Grid, Set.indicator, Finset.sum, TileStructure.Forest.𝓙', c, s, TileStructure.Forest.ijIntegral, Finset.univ, Membership.mem, Finset, Measurable.indicator, measurable_const, GridStructure.coeGrid_measurable
48 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma TileStructure.Forest.boundaryOperator_lt_top line 264 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, TileStructure.Forest, 𝔓, MeasureTheory.BoundedCompactSupport, MeasureTheory.MeasureSpace.volume, LT.lt and 3 more
Proof uses: Iff.mpr, Finset.sum, Grid, Finset.univ, Set.indicator, TileStructure.Forest.𝓙', c, s, TileStructure.Forest.ijIntegral, Membership.mem, Finset, ENNReal.sum_lt_top, dite, Classical.propDecidable, Eq.mpr, id, Eq, congrArg, Set.indicator_of_mem, TileStructure.Forest.ijIntegral_lt_top and 4 more
77 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
def TileStructure.Forest.𝓑 The indexing set for the collection of balls 𝓑, defined above Lemma 7.1.3 line 274 source
Source documentation
The indexing set for the collection of balls 𝓑, defined above Lemma 7.1.3.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, Prod, Grid
Proof uses: SProd.sprod, Set.Iic, HAdd.hAdd, OfNat.ofNat, HMul.hMul, Set.univ
35 instances, coercions and auxiliary constants left out.
```
def 𝓑 : Set (ℕ × ℕ × Grid X) := Iic (S + 5) ×ˢ Iic (2 * S + 3) ×ˢ univ
```
Mentions: Grid
def TileStructure.Forest.c𝓑 The center function for the collection of balls 𝓑 line 277 source
Source documentation
The center function for the collection of balls 𝓑.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, Prod, Grid
Proof uses: c, Prod.snd
28 instances, coercions and auxiliary constants left out.
```
def c𝓑 (z : ℕ × ℕ × Grid X) : X := c z.2.2
```
Mentions: Grid, c
def TileStructure.Forest.r𝓑 The radius function for the collection of balls 𝓑 line 280 source
Source documentation
The radius function for the collection of balls 𝓑.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, Prod, Grid
Proof uses: HMul.hMul, HPow.hPow, OfNat.ofNat, Prod.fst, HAdd.hAdd, s, Prod.snd
43 instances, coercions and auxiliary constants left out.
```
def r𝓑 (z : ℕ × ℕ × Grid X) : ℝ := 2 ^ z.1 * D ^ (s z.2.2 + z.2.1)
```
Mentions: Grid, s
lemma TileStructure.Forest.𝓑_finite line 282 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, Set.Finite, Prod, Grid, TileStructure.Forest.𝓑
Proof uses: Set.Finite.prod, Set.Iic, HAdd.hAdd, OfNat.ofNat, SProd.sprod, HMul.hMul, Set.univ, Set.finite_Iic, Set.finite_univ
40 instances, coercions and auxiliary constants left out.
lemma TileStructure.Forest.laverage_le_biInf_MB' line 285 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, Grid, LE.le, HAdd.hAdd, HMul.hMul, OfNat.ofNat and 20 more
Proof uses: id, Eq.mpr, iSup, Set.indicator, Inv.inv, congrArg, funext, iInf_congr_Prop, Iff.of_eq, Eq.refl, iSup_congr_Prop, congrFun', inv_one, Eq.trans, ENNReal.rpow_one, forall_congr, LE.le.trans, GridStructure.c, GridStructure.s, GridStructure.Grid_subset_ball and 4 more
142 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma TileStructure.Forest.laverage_le_biInf_MB line 294 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, Grid, LE.le, HMul.hMul, OfNat.ofNat, HPow.hPow and 18 more
Proof uses: TileStructure.Forest.laverage_le_biInf_MB', Eq.mpr, HAdd.hAdd, Dist.dist, id, congrArg, dist_self, add_zero
89 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma TileStructure.Forest.convex_scales Lemma 7.1.1, freely translated line 301 source
Source documentation
Lemma 7.1.1, freely translated.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, TileStructure.Forest, 𝔓, Membership.mem, Set.OrdConnected, Finset and 1 more
Proof uses: Eq.mpr, LE.le, Set.Icc, id, Eq, congrArg, propext, Set.ordConnected_def, Finset.image, 𝔰, Finset.filter, And, TileStructure.Forest.𝔗, E, Classical.propDecidable, Finset.univ, Exists, funext, congrFun', True and 37 more
77 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
```
lemma convex_scales (hu : u ∈ t) : OrdConnected (t.σ u x : Set ℤ) := by
…
```
lemma TileStructure.Forest.biUnion_𝓙 Part of Lemma 7.1.2 line 321 source
Source documentation
Part of Lemma 7.1.2

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, Eq, Set.iUnion, Grid, Membership.mem and 1 more
Proof uses: subset_antisymm, Set.iUnion₂_subset_iUnion, Eq.mpr, Exists, id, Eq.trans, congrArg, funext, Eq.mp, And, s, Neg.neg, Grid.exists_containing_subcube, And.intro, LE.le, le_rfl, And.left, scale_mem_Icc, Finset, Set.toFinset and 19 more
71 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
```
lemma biUnion_𝓙 : ⋃ J ∈ 𝓙 𝔖, J = ⋃ I : Grid X, (I : Set X) := by
…
```
Mentions: TileStructure.Forest.𝓙, Grid
lemma TileStructure.Forest.biUnion_𝓛 Part of Lemma 7.1.2 line 334 source
Source documentation
Part of Lemma 7.1.2

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, Eq, Set.iUnion, Grid, Membership.mem and 1 more
Proof uses: subset_antisymm, Set.iUnion₂_subset_iUnion, Eq.mpr, Exists, id, Eq.trans, congrArg, funext, Eq.mp, And, s, Neg.neg, Grid.exists_containing_subcube, And.intro, LE.le, le_rfl, And.left, scale_mem_Icc, Finset, Set.toFinset and 13 more
59 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
```
lemma biUnion_𝓛 : ⋃ J ∈ 𝓛 𝔖, J = ⋃ I : Grid X, (I : Set X) := by
…
```
Mentions: TileStructure.Forest.𝓛, Grid
lemma TileStructure.Forest.pairwiseDisjoint_𝓛 Part of Lemma 7.1.2 line 346 source
Source documentation
Part of Lemma 7.1.2

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, Set.PairwiseDisjoint, Grid, TileStructure.Forest.𝓛
Proof uses: Membership.mem, Ne, IsAntichain, LE.le, setOfPred_maximal_antichain, TileStructure.Forest.𝓛₀, Or.resolve_left, Disjoint, Or, le_or_ge_or_disjoint, Ne.symm
52 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma pairwiseDisjoint_𝓛 : (𝓛 𝔖).PairwiseDisjoint (fun I ↦ (I : Set X)) := fun I mI J mJ hn ↦ by
…
```
Mentions: TileStructure.Forest.𝓛
lemma TileStructure.Forest.exp_Lipschitz Used in the proof of exp_sub_one_le, which is used to prove Lemma 7.1.4 line 356 source
Source comment
Used in the proof of `exp_sub_one_le`, which is used to prove Lemma 7.1.4
```
private lemma exp_Lipschitz : LipschitzWith 1 (fun (t : ℝ) ↦ exp (.I * t)) := by
…
```
lemma TileStructure.Forest.exp_sub_one_le Used in the proof of Lemma 7.1.4 line 366 source
Source comment
Used in the proof of Lemma 7.1.4
```
private lemma exp_sub_one_le (t : ℝ) : ‖exp (.I * t) - 1‖ ≤ ‖t‖ := by
…
```
lemma TileStructure.Forest.dist_lt_5 Used in the proofs of Lemmas 7.1.4 and 7.1.5 line 371 source
Source comment
Used in the proofs of Lemmas 7.1.4 and 7.1.5
```
private lemma dist_lt_5 (hu : u ∈ t) (mp : p ∈ t.𝔗 u) (Qxp : Q x ∈ Ω p) :
    dist_(p) (𝒬 u) (Q x) < 5 := calc
…
```
Mentions: Ω

lemma TileStructure.Forest.L7_1_4_bound The bound in the third display in the proof of Lemma 7.1.4 line 380 source

Source comment

The bound in the third display in the proof of Lemma 7.1.4

private lemma L7_1_4_bound (hu : u ∈ t) {s : ℤ} (hs : s ∈ t.σ u x) {y : X} (hKxy : Ks s x y ≠ 0) :
    ‖exp (.I * (-𝒬 u y + Q x y + 𝒬 u x - Q x x)) - 1‖ₑ ≤
    5 * 2 ^ (4 * a) * 2 ^ (s - σMax t u x ⟨s, hs⟩) := by
…

Mentions: s, Ks, TileStructure.Forest.σMax

lemma TileStructure.Forest.L7_1_4_integrand_bound line 438 source
lemma TileStructure.Forest.sum_pow_two_le The geometric sum used to prove L7_1_4_sum line 455 source
Source comment
The geometric sum used to prove `L7_1_4_sum`
```
private lemma sum_pow_two_le (a b : ℤ) : ∑ s ∈ Finset.Icc a b, (2 : ℝ≥0∞) ^ s ≤ 2 ^ (b + 1) := by
…
```
Mentions: s
lemma TileStructure.Forest.L7_1_4_sum The sum used in the proof of Lemma 7.1.4 line 478 source
Source comment
The sum used in the proof of Lemma 7.1.4
```
private lemma L7_1_4_sum (hσ : (t.σ u x).Nonempty) :
    ∑ s ∈ t.σ u x, (2 : ℝ≥0∞) ^ (s - t.σMax u x hσ) ≤ 2 := by
…
```
Mentions: s

lemma TileStructure.Forest.L7_1_4_dist_le Inequality used twice in the proof of Lemma 7.1.4 line 491 source

Source comment

Inequality used twice in the proof of Lemma 7.1.4

private lemma L7_1_4_dist_le {p : 𝔓 X} (xp : x ∈ E p) {J : Grid X}
    (hJ : ((J : Set X) ∩ ball x (D ^ 𝔰 p / 2)).Nonempty) :
    dist (c J) (𝔠 p) ≤ 4 * D ^ (s J) + 4.5 * D ^ (𝔰 p) := by
…

Mentions: 𝔓, E, Grid, 𝔰, c, 𝔠, s

lemma TileStructure.Forest.s_le_s Inequality needed for the proof of L7_1_4_integral_le_integral line 506 source
Source comment
Inequality needed for the proof of `L7_1_4_integral_le_integral`
```
private lemma s_le_s {p : 𝔓 X} (pu : p ∈ t.𝔗 u) (xp : x ∈ E p)
    {J : Grid X} (hJ : J ∈ 𝓙 (t.𝔗 u) ∧ ((J : Set X) ∩ ball x (D ^ 𝔰 p / 2)).Nonempty) :
    s J ≤ 𝔰 p := by
…
```
Mentions: 𝔓, E, Grid, TileStructure.Forest.𝓙, 𝔰, s
lemma TileStructure.Forest.ball_covered_by_𝓙 line 523 source
lemma TileStructure.Forest.Grid_subset_ball' line 531 source

lemma TileStructure.Forest.L7_1_4_integral_le_integral The integral bound needed for the proof of Lemma 7.1.4 line 541 source

Source comment

The integral bound needed for the proof of Lemma 7.1.4

private lemma L7_1_4_integral_le_integral (hu : u ∈ t) (hf : BoundedCompactSupport f) {p : 𝔓 X}
    (pu : p ∈ t u) (xp : x ∈ E p) : ∫⁻ y in ball x (D ^ 𝔰 p / 2), ‖f y‖ₑ ≤
    ∫⁻ y in ball (𝔠 p) (16 * D ^ 𝔰 p), ‖approxOnCube (𝓙 (t u)) (‖f ·‖) y‖ₑ := by
…

Mentions: 𝔓, E, 𝔰, 𝔠, TileStructure.Forest.approxOnCube, TileStructure.Forest.𝓙

lemma TileStructure.Forest.L7_1_4_laverage_le_MB An average over ball (𝔠 p) (16 * D ^ 𝔰 p) is bounded by MB; needed for Lemma 7.1.4 line 582 source
Source comment
An average over `ball (𝔠 p) (16 * D ^ 𝔰 p)` is bounded by `MB`; needed for Lemma 7.1.4
```
private lemma L7_1_4_laverage_le_MB (hL : L ∈ 𝓛 (t u)) (hx : x ∈ L) (hx' : x' ∈ L) (g : X → ℝ)
    {p : 𝔓 X} (pu : p ∈ t.𝔗 u) (xp : x ∈ E p) :
    (∫⁻ y in ball (𝔠 p) (16 * D ^ 𝔰 p), ‖g y‖ₑ) / volume (ball (𝔠 p) (16 * D ^ 𝔰 p)) ≤
    maximalFunction volume 𝓑 c𝓑 r𝓑 1 g x' := by
…
```
Mentions: TileStructure.Forest.𝓛, g, 𝔓, E, 𝔠, 𝔰, TileStructure.Forest.𝓑, TileStructure.Forest.c𝓑, TileStructure.Forest.r𝓑
lemma TileStructure.Forest.first_tree_pointwise Lemma 7.1.4 line 602 source
Source documentation
Lemma 7.1.4

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, TileStructure.Forest, 𝔓, Grid, Membership.mem, TileStructure.Forest.𝓛 and 29 more
Proof uses: MulPosReflectLE, inferInstance, PosMulReflectLE, Eq.mpr, id, Eq, congrArg, rfl, Finset, EmptyCollection.emptyCollection, Finset.Nonempty, Or, Finset.eq_empty_or_nonempty, of_eq_true, HPow.hPow, 𝕔, Eq.trans, True, congrFun', enorm_zero and 191 more
336 instances, coercions and auxiliary constants left out.

Tactic trace: 70 steps
Open to load the checked before-and-after goal states.
```
lemma first_tree_pointwise (hu : u ∈ t) (hL : L ∈ 𝓛 (t u)) (hx : x ∈ L) (hx' : x' ∈ L)
    (hf : BoundedCompactSupport f) :
    ‖∑ i ∈ t.σ u x, ∫ y, (exp (.I * (-𝒬 u y + Q x y + 𝒬 u x - Q x x)) - 1) * Ks i x y * f y‖ₑ ≤
    C7_1_4 a * maximalFunction volume 𝓑 c𝓑 r𝓑 1 (approxOnCube (𝓙 (t u)) (‖f ·‖)) x' := by
…
```
Mentions: TileStructure.Forest.𝓛, Ks, TileStructure.Forest.𝓑, TileStructure.Forest.c𝓑, TileStructure.Forest.r𝓑, TileStructure.Forest.approxOnCube, TileStructure.Forest.𝓙
lemma TileStructure.Forest.second_tree_pointwise Lemma 7.1.5 line 671 source
Source documentation
Lemma 7.1.5

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, TileStructure.Forest, 𝔓, Grid, Membership.mem, TileStructure.Forest.𝓛 and 14 more
Proof uses: Eq, Finset, EmptyCollection.emptyCollection, Finset.Nonempty, Or, Finset.eq_empty_or_nonempty, of_eq_true, HPow.hPow, OfNat.ofNat, 𝕔, Eq.trans, True, congrFun', congrArg, Finset.sum_congr, Eq.refl, enorm_zero, Finset.min', Finset.min'_mem, And and 229 more
328 instances, coercions and auxiliary constants left out.

Tactic trace: 106 steps
Open to load the checked before-and-after goal states.
```
lemma second_tree_pointwise (hu : u ∈ t) (hL : L ∈ 𝓛 (t u)) (hx : x ∈ L) (hx' : x' ∈ L) :
    ‖∑ i ∈ t.σ u x, ∫ y, Ks i x y * approxOnCube (𝓙 (t u)) f y‖ₑ ≤
    nontangentialMaximalFunction (𝒬 u) (approxOnCube (𝓙 (t u)) f) x' := by
…
```
Mentions: TileStructure.Forest.𝓛, Ks, TileStructure.Forest.approxOnCube, TileStructure.Forest.𝓙, TileStructure.Forest.nontangentialMaximalFunction
lemma TileStructure.Forest.p_sum_eq_s_sum line 761 source

lemma TileStructure.Forest.L7_1_6_integral_eq Equation 7.1.10 from the blueprint line 794 source

Source comment

Equation 7.1.10 from the blueprint

private lemma L7_1_6_integral_eq {J : Grid X} (hJ : J ∈ 𝓙 (t.𝔗 u)) {i : ℤ}
    (hf : BoundedCompactSupport f) : ∫ y in J, Ks i x y * (f y - approxOnCube (𝓙 (t u)) f y) =
    ∫ y in J, (⨍ z in J, (Ks i x y - Ks i x z)) * f y := by
…

Mentions: Grid, TileStructure.Forest.𝓙, Ks, TileStructure.Forest.approxOnCube

lemma TileStructure.Forest.L7_1_6_integral_le Integral norm bound used implicitly in the third display of the proof of Lemma 7.1.6 line 841 source
Source comment
Integral norm bound used implicitly in the third display of the proof of Lemma 7.1.6.
```
private lemma L7_1_6_integral_le {J : Grid X} (hJ : J ∈ 𝓙 (t u)) {i : ℤ}
    (hf : BoundedCompactSupport f) : ‖∫ y in J, Ks i x y * (f y - approxOnCube (𝓙 (t u)) f y)‖ₑ ≤
    D2_1_3 a / volume (ball x (D ^ i)) * 2 ^ (3 / a : ℝ) *
    (D ^ ((s J - i) / (a : ℝ)) * ∫⁻ y in J, ‖f y‖ₑ) := by
…
```
Mentions: Grid, TileStructure.Forest.𝓙, Ks, TileStructure.Forest.approxOnCube, D2_1_3, s

lemma TileStructure.Forest.L7_1_6_I_le Prove an upper bound for the function I used in the proof of Lemma 7.1.6 line 891 source

Source comment

Prove an upper bound for the function `I` used in the proof of Lemma 7.1.6

private lemma L7_1_6_I_le (hu : u ∈ t) (hf : BoundedCompactSupport f) {p : 𝔓 X} (hp : p ∈ t u)
    {x : X} (hxp : x ∈ E p) : ‖∫ y, Ks (𝔰 p) x y * (f y - approxOnCube (𝓙 (t u)) f y)‖ₑ ≤
    D2_1_3 a / volume (ball x (D ^ 𝔰 p)) * 2 ^ (3 / a : ℝ) *
    ∑ J ∈ 𝓙' t u (𝔠 p) (𝔰 p), (D : ℝ≥0∞) ^ ((s J - 𝔰 p) / (a : ℝ)) * ∫⁻ y in J, ‖f y‖ₑ := by
…

Mentions: 𝔓, E, Ks, 𝔰, TileStructure.Forest.approxOnCube, TileStructure.Forest.𝓙, D2_1_3, 𝔠, s

lemma TileStructure.Forest.sum_p_eq_sum_I_sum_p line 928 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, TileStructure.Forest, 𝔓, ENNReal, Eq, Finset.sum and 16 more
Proof uses: Finset, Trans.trans, Finset.biUnion, Finset.ext, Eq.mpr, Iff, Exists, id, congr, congrArg, Eq.trans, congrFun', Finset.filter_congr, Iff.of_eq, Eq.refl, True, true_and, funext, Iff.intro, And.intro and 18 more
70 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
lemma TileStructure.Forest.le_C7_1_6 line 954 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, ENNReal, HMul.hMul, D2_1_3, HPow.hPow, defaultA, Real, HDiv.hDiv, TileStructure.Forest.C7_1_6
Proof uses: id, NNReal, HAdd.hAdd, 𝕔, Eq.mpr, Eq, congrArg, TileStructure.Forest.C7_1_6_def, congrFun', Nat.cast_pow, Trans.trans, mul_le_mul_right, Eq.rec, Eq.refl, Eq.trans, Eq.symm, ENNReal.rpow_one, ENNReal.rpow_le_rpow_of_exponent_le, one_le_two, propext and 41 more
137 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
lemma TileStructure.Forest.third_tree_pointwise Lemma 7.1.6 line 974 source
Source documentation
Lemma 7.1.6

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, TileStructure.Forest, 𝔓, Grid, Membership.mem, TileStructure.Forest.𝓛 and 17 more
Proof uses: Finset, Set.toFinset, Set.ofPred, And, Metric.ball, OfNat.ofNat, HPow.hPow, 𝔰, s, Classical.propDecidable, Finset.filter, Eq, 𝓘, Finset.univ, GT.gt, pow_pos, of_eq_true, LT.lt, Eq.trans, True and 184 more
288 instances, coercions and auxiliary constants left out.

Tactic trace: 76 steps
Open to load the checked before-and-after goal states.
```
lemma third_tree_pointwise (hu : u ∈ t) (hL : L ∈ 𝓛 (t u)) (hx : x ∈ L) (hx' : x' ∈ L)
    (hf : BoundedCompactSupport f) :
    ‖∑ i ∈ t.σ u x, ∫ y, Ks i x y * (f y - approxOnCube (𝓙 (t u)) f y)‖ₑ ≤
    C7_1_6 a * t.boundaryOperator u (approxOnCube (𝓙 (t u)) (‖f ·‖)) x' := by
…
```
Mentions: TileStructure.Forest.𝓛, Ks, TileStructure.Forest.approxOnCube, TileStructure.Forest.𝓙
lemma TileStructure.Forest.C7_1_6_le_C7_1_3 line 1071 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, NNReal, TileStructure.Forest.C7_1_6, TileStructure.Forest.C7_1_3
Proof uses: Eq.mpr, HPow.hPow, OfNat.ofNat, HMul.hMul, HAdd.hAdd, 𝕔, HDiv.hDiv, id, Eq, congrArg, TileStructure.Forest.C7_1_6_def, TileStructure.Forest.C7_1_3_def, pow_le_pow_right₀, Mathlib.Meta.NormNum.isNat_le_true, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_one, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Bool, Bool.true and 3 more
45 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma TileStructure.Forest.C7_1_4_le_C7_1_3 line 1077 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, NNReal, TileStructure.Forest.C7_1_4, TileStructure.Forest.C7_1_3
Proof uses: HPow.hPow, Mathlib.Meta.NormNum.isNat_le_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Mathlib.Meta.NormNum.isNat_pow, Mathlib.Meta.NormNum.IsNatPowT.run, Mathlib.Meta.NormNum.IsNatPowT.trans, Eq, Nat.pow, Mathlib.Meta.NormNum.IsNatPowT.bit0, Bool, Bool.true, Eq.mpr, HMul.hMul, HAdd.hAdd, 𝕔, congrArg, TileStructure.Forest.C7_1_4_def, HDiv.hDiv and 89 more
112 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
lemma TileStructure.Forest.pointwise_tree_estimate Lemma 7.1.3 line 1092 source
Source documentation
Lemma 7.1.3.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, TileStructure.Forest, 𝔓, Grid, Membership.mem, TileStructure.Forest.𝓛 and 26 more
Proof uses: Eq.mpr, id, Eq, congrArg, rfl, Finset.sum, Finset.filter, Classical.propDecidable, Finset.univ, carlesonOn, Set.indicator, E, MeasureTheory.integral, HSub.hSub, MeasureTheory.SimpleFunc, Ks, 𝔰, TileStructure.Forest.σ, of_eq_true, Eq.trans and 130 more
304 instances, coercions and auxiliary constants left out.

Tactic trace: 55 steps
Open to load the checked before-and-after goal states.
```
lemma pointwise_tree_estimate (hu : u ∈ t) (hL : L ∈ 𝓛 (t u)) (hx : x ∈ L) (hx' : x' ∈ L)
    (hf : BoundedCompactSupport f) :
    ‖carlesonSum (t u) (fun y ↦ exp (.I * - 𝒬 u y) * f y) x‖ₑ ≤
    C7_1_3 a * (maximalFunction volume 𝓑 c𝓑 r𝓑 1 (approxOnCube (𝓙 (t u)) (‖f ·‖)) x' +
    t.boundaryOperator u (approxOnCube (𝓙 (t u)) (‖f ·‖)) x') +
    nontangentialMaximalFunction (𝒬 u) (approxOnCube (𝓙 (t u)) f) x' := by
…
```
Mentions: TileStructure.Forest.𝓛, carlesonSum, TileStructure.Forest.𝓑, TileStructure.Forest.c𝓑, TileStructure.Forest.r𝓑, TileStructure.Forest.approxOnCube, TileStructure.Forest.𝓙, TileStructure.Forest.nontangentialMaximalFunction