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

16 declarations, 0 contain sorry, 0 declared as axioms

Section 7.4 except Lemmas 4-6

Imports (1)

Carleson.ForestOperator.QuantativeEstimate

Imported by 3 files

def TileStructure.Forest.adjointBoundaryOperator The operator S_{2,𝔲} f(x), given above Lemma 7.4.3 line 25 source
Source documentation
The operator S_{2,𝔲} f(x), given above Lemma 7.4.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, 𝔓, ENNReal
Proof uses: HAdd.hAdd, ENorm.enorm, adjointCarlesonSum, TileStructure.Forest.𝔗, maximalFunction, Prod, Grid, MeasureTheory.MeasureSpace.volume, TileStructure.Forest.𝓑, TileStructure.Forest.c𝓑, TileStructure.Forest.r𝓑, OfNat.ofNat
45 instances, coercions and auxiliary constants left out.
```
def adjointBoundaryOperator (u : 𝔓 X) (f : X → ℂ) (x : X) : ℝ≥0∞ :=
…
```
Mentions: 𝔓
def TileStructure.Forest.𝔖₀ The set 𝔖 defined in the proof of Lemma 7.4.4 line 31 source
Source documentation
The set 𝔖 defined in the proof of Lemma 7.4.4. We append a subscript 0 to distinguish it from the section variable.

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, 𝔓
Proof uses: Set.ofPred, And, Membership.mem, Union.union, TileStructure.Forest.𝔗, LE.le, HPow.hPow, OfNat.ofNat, HDiv.hDiv, HMul.hMul, defaultZ, Dist.dist, WithFunctionDistance, 𝔠, 𝔰, PreTileStructure.𝒬
44 instances, coercions and auxiliary constants left out.
```
def 𝔖₀ : Set (𝔓 X) := { p ∈ t u₁ ∪ t u₂ | 2 ^ ((Z : ℝ) * n / 2) ≤ dist_(p) (𝒬 u₁) (𝒬 u₂) }
```
Mentions: 𝔓
lemma TileStructure.Forest.adjoint_tile_support1 Part 1 of Lemma 7.4.1 line 35 source
Source documentation
Part 1 of Lemma 7.4.1. Todo: update blueprint with precise properties needed on the function.

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, adjointCarleson, Set.indicator, Metric.ball and 6 more
Proof uses: Eq.mpr, id, congrArg, adjoint_eq_adjoint_indicator, E_subset_𝓘, funext, Ne, Or, eq_or_ne, Eq.symm, Iff.mpr, Not, Membership.mem, Set.indicator_apply_eq_self, Set.indicator_of_mem, And, Grid, Ks, Exists, Mathlib.Tactic.Contrapose.contrapose₂ and 50 more
178 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
```
lemma adjoint_tile_support1 : adjointCarleson p f =
    (ball (𝔠 p) (5 * D ^ 𝔰 p)).indicator (adjointCarleson p ((𝓘 p : Set X).indicator f)) := by
…
```
Mentions: adjointCarleson, 𝔠, 𝔰, 𝓘
lemma TileStructure.Forest.adjoint_tile_support2 Part 2 of Lemma 7.4.1 line 57 source
Source documentation
Part 2 of Lemma 7.4.1. Todo: update blueprint with precise properties needed on the function.

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, TileStructure.Forest.𝔗, Eq and 3 more
Proof uses: Eq.mpr, id, congrArg, Eq.symm, adjoint_eq_adjoint_indicator, LE.le.trans, E, E_subset_𝓘, And.left, LE.le, Prod.fst, GridStructure.Grid, Prod.mk, GridStructure.s, Grid, OrderDual, FunctionDistances.Θ, smul, OfNat.ofNat, Prod.snd and 22 more
96 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma adjoint_tile_support2 (hu : u ∈ t) (hp : p ∈ t u) : adjointCarleson p f =
    (𝓘 u : Set X).indicator (adjointCarleson p ((𝓘 u : Set X).indicator f)) := by
…
```
Mentions: adjointCarleson, 𝓘
lemma TileStructure.Forest.adjoint_tile_support2_sum line 63 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, 𝔓, Membership.mem, Eq, adjointCarlesonSum and 3 more
Proof uses: id, Trans.trans, Finset.sum, Finset.filter, Classical.propDecidable, Finset.univ, adjointCarleson, funext, Eq.mpr, congr, congrArg, Finset.sum_congr, Finset.filter_congr, Finset, Iff.of_eq, Eq.refl, Eq.trans, congrFun, Finset.sum_apply, TileStructure.Forest.adjoint_tile_support2 and 7 more
47 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma TileStructure.Forest.adjoint_tile_support2_sum_partial A partially applied variant of adjoint_tile_support2_sum, used to prove Lemma 7.7.3 line 76 source
Source documentation
A partially applied variant of adjoint_tile_support2_sum, used to prove Lemma 7.7.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, 𝔓, Membership.mem, Eq, adjointCarlesonSum and 3 more
Proof uses: id, funext, Finset.sum, Finset.filter, Classical.propDecidable, Finset.univ, adjointCarleson, Finset.sum_congr, Eq.refl, Finset, Eq.mpr, congrArg, Eq.symm, adjoint_eq_adjoint_indicator, LE.le.trans, E, E_subset_𝓘, And.left, LE.le, Prod.fst and 13 more
64 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma adjoint_tile_support2_sum_partial (hu : u ∈ t) :
    adjointCarlesonSum (t u) f = (adjointCarlesonSum (t u) ((𝓘 u : Set X).indicator f)) := by
…
```
Mentions: adjointCarlesonSum, 𝓘
lemma TileStructure.Forest.enorm_adjointCarleson_le line 82 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, ENNReal, ENorm.enorm, adjointCarleson and 13 more
Proof uses: Trans.trans, Ks, Eq, RingHom, starRingEnd, Complex.exp, Complex.I, HSub.hSub, FunctionDistances.Θ, MeasureTheory.SimpleFunc, MeasureTheory.enorm_integral_le_lintegral_enorm, eq_of_heq, MeasurableSpace, HEq, Eq.refl, HEq.refl, Eq.symm, funext, Eq.mpr, id and 54 more
236 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
lemma TileStructure.Forest.enorm_adjointCarleson_le_mul_indicator line 106 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, ENNReal, ENorm.enorm, adjointCarleson and 14 more
Proof uses: Eq.mpr, 𝓘, id, Eq, congrArg, TileStructure.Forest.adjoint_tile_support1, enorm_indicator_eq_indicator_enorm, Trans.trans, Set.indicator_le_indicator, TileStructure.Forest.enorm_adjointCarleson_le, Eq.rec, Eq.refl, funext, Eq.trans, Eq.symm, mul_one, Set.indicator_const_mul, HMul, MeasureTheory.setLIntegral_congr_fun, measurableSet_E and 17 more
173 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
lemma TileStructure.Forest.adjoint_density_tree_bound1 line 125 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, LE.le and 16 more
Proof uses: Eq.mpr, carlesonSum, id, Eq, congrArg, Eq.symm, adjointCarlesonSum_adjoint, TileStructure.Forest.density_tree_bound1
114 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma TileStructure.Forest.adjoint_tree_estimate Part 1 of Lemma 7.4.2 line 132 source
Source documentation
Part 1 of Lemma 7.4.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, TileStructure.Forest, 𝔓, MeasureTheory.BoundedCompactSupport, MeasureTheory.MeasureSpace.volume, LE.le and 12 more
Proof uses: dite, Eq, Eq.mpr, id, congrArg, zero_le, Not, MeasureTheory.BoundedCompactSupport.adjointCarlesonSum, Eq.symm, propext, ENNReal.mul_le_mul_iff_left, MeasureTheory.MemLp.eLpNorm_ne_top, MeasureTheory.BoundedCompactSupport.memLp, sq, ENorm.enorm, MeasureTheory.integral, RingHom, starRingEnd, MeasureTheory.eLpNorm_two_eq_enorm_integral_mul_conj, mul_assoc and 6 more
145 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
lemma adjoint_tree_estimate
    (hg : BoundedCompactSupport g) (h2g : support g ⊆ G) (hu : u ∈ t) :
    eLpNorm (adjointCarlesonSum (t u) g) 2 volume ≤
    C7_3_1_1 a * dens₁ (t u) ^ (2 : ℝ)⁻¹ * eLpNorm g 2 volume := by
…
```
Mentions: g, adjointCarlesonSum, dens₁
lemma TileStructure.Forest.adjoint_density_tree_bound2 line 145 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, LE.le and 17 more
Proof uses: Eq.mpr, carlesonSum, id, Eq, congrArg, Eq.symm, adjointCarlesonSum_adjoint, TileStructure.Forest.density_tree_bound2
114 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma TileStructure.Forest.indicator_adjoint_tree_estimate Part 2 of Lemma 7.4.2 line 154 source
Source documentation
Part 2 of Lemma 7.4.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, TileStructure.Forest, 𝔓, MeasureTheory.BoundedCompactSupport, MeasureTheory.MeasureSpace.volume, LE.le and 14 more
Proof uses: dite, Eq, Eq.mpr, id, congrArg, zero_le, Not, MeasureTheory.BoundedCompactSupport.indicator, MeasureTheory.BoundedCompactSupport.adjointCarlesonSum, ProofData.measurableSet_F, Eq.symm, propext, ENNReal.mul_le_mul_iff_left, MeasureTheory.MemLp.eLpNorm_ne_top, MeasureTheory.BoundedCompactSupport.memLp, sq, ENorm.enorm, MeasureTheory.integral, RingHom, starRingEnd and 21 more
182 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
lemma indicator_adjoint_tree_estimate
    (hg : BoundedCompactSupport g) (h2g : support g ⊆ G) (hu : u ∈ t) :
    eLpNorm (F.indicator (adjointCarlesonSum (t u) g)) 2 ≤
    C7_3_1_2 a * dens₁ (t u) ^ (2 : ℝ)⁻¹ * dens₂ (t u) ^ (2 : ℝ)⁻¹ * eLpNorm g 2 := by
…
```
Mentions: g, adjointCarlesonSum, dens₁, dens₂
lemma TileStructure.Forest.le_C7_4_3 line 177 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, NNReal, HAdd.hAdd, TileStructure.Forest.C7_3_1_1, CMB, defaultA, TileStructure.Forest.C7_4_3
Proof uses: Eq.mpr, HPow.hPow, HMul.hMul, 𝕔, HDiv.hDiv, id, Eq, congrArg, TileStructure.Forest.C7_4_3_def, TileStructure.Forest.C7_3_1_1_def, Real, CMB_defaultA_two_eq, Trans.trans, add_le_add, le_refl, NNReal.one_le_rpow, one_le_two, le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl and 143 more
191 instances, coercions and auxiliary constants left out.

Tactic trace: 46 steps
Open to load the checked before-and-after goal states.
lemma TileStructure.Forest.adjoint_tree_control Lemma 7.4.3 line 214 source
Source documentation
Lemma 7.4.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, 𝔓, Membership.mem, MeasureTheory.BoundedCompactSupport, MeasureTheory.MeasureSpace.volume and 8 more
Proof uses: MeasureTheory.AEStronglyMeasurable, ENorm.enorm, adjointCarlesonSum, TileStructure.Forest.𝔗, AEMeasurable.aestronglyMeasurable, MeasureTheory.AEStronglyMeasurable.enorm, MeasureTheory.AEStronglyMeasurable.adjointCarlesonSum, MeasureTheory.BoundedCompactSupport.aestronglyMeasurable, maximalFunction, Prod, Grid, TileStructure.Forest.𝓑, TileStructure.Forest.c𝓑, TileStructure.Forest.r𝓑, Measurable.aestronglyMeasurable, measurable_maximalFunction, Trans.trans, HAdd.hAdd, TileStructure.Forest.C7_3_1_1, HPow.hPow and 40 more
210 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
```
lemma adjoint_tree_control
    (hu : u ∈ t) (hf : BoundedCompactSupport f) (h2f : f.support ⊆ G) :
    eLpNorm (adjointBoundaryOperator t u f ·) 2 volume ≤ C7_4_3 a * eLpNorm f 2 volume := by
…
```
Mentions: TileStructure.Forest.adjointBoundaryOperator
lemma TileStructure.Forest.overlap_implies_distance Part 1 of Lemma 7.4.7 line 243 source
Source documentation
Part 1 of Lemma 7.4.7.

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, Ne, LE.le and 7 more
Proof uses: id, Eq.mpr, Set.ofPred, And, HPow.hPow, OfNat.ofNat, HDiv.hDiv, HMul.hMul, defaultZ, Dist.dist, WithFunctionDistance, 𝔠, 𝔰, PreTileStructure.𝒬, Eq, True, congrFun', congrArg, eq_true, true_and and 78 more
194 instances, coercions and auxiliary constants left out.

Tactic trace: 56 steps
Open to load the checked before-and-after goal states.
```
lemma overlap_implies_distance (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (hu : u₁ ≠ u₂)
    (h2u : 𝓘 u₁ ≤ 𝓘 u₂) (hp : p ∈ t u₁ ∪ t u₂)
    (hpu₁ : ¬Disjoint (𝓘 p : Set X) (𝓘 u₁)) : p ∈ 𝔖₀ t u₁ u₂ := by
…
```
Mentions: 𝓘, TileStructure.Forest.𝔖₀
lemma TileStructure.Forest.𝔗_subset_𝔖₀ Part 2 of Lemma 7.4.7 line 291 source
Source documentation
Part 2 of Lemma 7.4.7.

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, Ne, LE.le and 4 more
Proof uses: TileStructure.Forest.overlap_implies_distance, Set.mem_union_left, Set.Nonempty, Not, Disjoint, Grid.nonempty, Iff.mpr, Exists, And, Set.not_disjoint_iff, Exists.intro, And.intro, And.left, Prod.fst, GridStructure.Grid, Prod.mk, GridStructure.s, OrderDual, FunctionDistances.Θ, smul and 3 more
72 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma 𝔗_subset_𝔖₀ (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (hu : u₁ ≠ u₂) (h2u : 𝓘 u₁ ≤ 𝓘 u₂) :
    t u₁ ⊆ 𝔖₀ t u₁ u₂ := fun p mp ↦ by
…
```
Mentions: 𝓘, TileStructure.Forest.𝔖₀