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

19 declarations, 0 contain sorry, 0 declared as axioms

Section 7.6 and Lemma 7.4.6

Imports (2)

Imported by 2 files

def TileStructure.Forest.𝓙₆ The definition 𝓙' at the start of Section 7.6 line 27 source
Source documentation
The definition 𝓙' at the start of Section 7.6. We use a different notation to distinguish it from the 𝓙' used in Section 7.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
Proof uses: Inter.inter, TileStructure.Forest.𝓙, TileStructure.Forest.𝔗, Set.Iic, 𝓘
31 instances, coercions and auxiliary constants left out.
```
def 𝓙₆ : Set (Grid X) := 𝓙 (t u₁) ∩ Iic (𝓘 u₁)
```
Mentions: Grid, TileStructure.Forest.𝓙, 𝓘
lemma TileStructure.Forest.union_𝓙₆ Part of Lemma 7.6.1 line 31 source
Source documentation
Part of Lemma 7.6.1.

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, Set.iUnion and 3 more
Proof uses: subset_antisymm, Iff.mpr, LE.le, Set.iUnion₂_subset_iff, And.left, Prod.fst, GridStructure.Grid, Prod.mk, GridStructure.s, Prod.snd, And.right, TileStructure.Forest.𝓙, TileStructure.Forest.𝔗, Set.Iic, Eq.mpr, id, congrArg, TileStructure.Forest.biUnion_𝓙, Set.subset_iUnion_of_subset, le_refl and 117 more
164 instances, coercions and auxiliary constants left out.

Tactic trace: 51 steps
Open to load the checked before-and-after goal states.
```
lemma union_𝓙₆ (hu₁ : u₁ ∈ t) : ⋃ J ∈ 𝓙₆ t u₁, (J : Set X) = 𝓘 u₁ := by
…
```
Mentions: TileStructure.Forest.𝓙₆, 𝓘
lemma TileStructure.Forest.pairwiseDisjoint_𝓙₆ Part of Lemma 7.6.1 line 86 source
Source documentation
Part of Lemma 7.6.1.

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, 𝔓, Set.PairwiseDisjoint, Grid, TileStructure.Forest.𝓙₆
Proof uses: LE.le, Inter.inter, TileStructure.Forest.𝓙, TileStructure.Forest.𝔗, Set.Iic, 𝓘, Set.inter_subset_left, Set.PairwiseDisjoint.subset, TileStructure.Forest.pairwiseDisjoint_𝓙
52 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma pairwiseDisjoint_𝓙₆ : (𝓙₆ t u₁).PairwiseDisjoint (fun I ↦ (I : Set X)) := by
…
```
Mentions: TileStructure.Forest.𝓙₆
lemma TileStructure.Forest.nonneg_C7_6_3_add_two line 95 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Real, OfNat.ofNat, HAdd.hAdd, TileStructure.Forest.C7_6_3
Proof uses: Eq.mpr, HSub.hSub, HDiv.hDiv, HMul.hMul, defaultZ, 𝕔, HPow.hPow, id, Eq, congrArg, congrFun', TileStructure.Forest.C7_6_3_def, sub_add_cancel, div_nonneg, mul_nonneg, Nat.cast_nonneg', le_of_lt, Right.add_pos_of_nonneg_of_pos, Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat and 5 more
68 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma TileStructure.Forest.thin_scale_impact_prelims Some preliminary relations for Lemma 7.6.3 line 99 source
Source documentation
Some preliminary relations for Lemma 7.6.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 21 more
Proof uses: Trans.trans, MeasureTheory.dist_lt_of_not_disjoint_ball, Eq.mpr, id, congrFun', congrArg, congr, add_le_add, mul_le_mul_of_nonneg_left, Real.rpow_le_rpow_of_exponent_le, one_le_realD, add_assoc, propext, le_add_iff_nonneg_right, TileStructure.Forest.nonneg_C7_6_3_add_two, le_of_lt, Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo and 116 more
221 instances, coercions and auxiliary constants left out.

Tactic trace: 47 steps
Open to load the checked before-and-after goal states.
```
lemma thin_scale_impact_prelims (hu₁ : u₁ ∈ t) (hJ : J ∈ 𝓙₆ t u₁)
    (hd : ¬Disjoint (ball (𝔠 p) (8 * D ^ 𝔰 p)) (ball (c J) (8 * D ^ s J)))
    (h : s J - C7_6_3 a n < 𝔰 p) :
    dist (𝔠 p) (c J) < 16 * D ^ (𝔰 p + C7_6_3 a n + 2) ∧
    ∃ J', J < J' ∧ s J' = s J + 1 ∧
      ∃ p ∈ t u₁, ↑(𝓘 p) ⊆ ball (c J') (100 * D ^ (s J' + 1)) := by
…
```
Mentions: TileStructure.Forest.𝓙₆, 𝔠, 𝔰, c, s, 𝓘
lemma TileStructure.Forest.thin_scale_impact_key The key relation of Lemma 7.6.3, which will eventually be shown to lead to a contradiction line 134 source
Source documentation
The key relation of Lemma 7.6.3, which will eventually be shown to lead to a contradiction.

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, Ne and 23 more
Proof uses: Dist.dist, Exists, And, Eq, TileStructure.Forest.thin_scale_impact_prelims, Eq.mpr, id, congrArg, Eq.symm, mul_one, mul_le_mul', four_le_Z, Nat.le_add_left, Trans.trans, Nat.ceil, WithFunctionDistance, PreTileStructure.𝒬, Nat.sub_add_cancel, pow_succ, mul_two and 185 more
274 instances, coercions and auxiliary constants left out.

Tactic trace: 59 steps
Open to load the checked before-and-after goal states.
```
lemma thin_scale_impact_key (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (hu : u₁ ≠ u₂)
    (h2u : 𝓘 u₁ ≤ 𝓘 u₂) (hp : p ∈ t u₂ \ 𝔖₀ t u₁ u₂) (hJ : J ∈ 𝓙₆ t u₁)
    (hd : ¬Disjoint (ball (𝔠 p) (8 * D ^ 𝔰 p)) (ball (c J) (8 * D ^ s J)))
    (h : s J - C7_6_3 a n < 𝔰 p) :
    (2 : ℝ) ^ (Z * (n + 1) - 1) <
    2 ^ (a * (𝕔 * a ^ 2 * (C7_6_3 a n + 2 + 1) + 9)) * 2 ^ ((Z : ℝ) * n / 2) := by
…
```
Mentions: 𝓘, TileStructure.Forest.𝔖₀, TileStructure.Forest.𝓙₆, 𝔠, 𝔰, c, s
lemma TileStructure.Forest.thin_scale_impact Lemma 7.6.3 line 192 source
Source documentation
Lemma 7.6.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, Ne and 18 more
Proof uses: Decidable.byContradiction, defaultZ, HAdd.hAdd, Eq.mpr, id, Eq, congrArg, Eq.symm, mul_one, mul_le_mul', four_le_Z, Nat.le_add_left, LT.lt, 𝕔, HDiv.hDiv, TileStructure.Forest.thin_scale_impact_key, Eq.mp, False, Eq.trans, Nat.cast_zero and 189 more
298 instances, coercions and auxiliary constants left out.

Tactic trace: 46 steps
Open to load the checked before-and-after goal states.
```
lemma thin_scale_impact (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (hu : u₁ ≠ u₂)
    (h2u : 𝓘 u₁ ≤ 𝓘 u₂) (hp : p ∈ t u₂ \ 𝔖₀ t u₁ u₂) (hJ : J ∈ 𝓙₆ t u₁)
    (hd : ¬Disjoint (ball (𝔠 p) (8 * D ^ 𝔰 p)) (ball (c J) (8 * D ^ s J))) :
    𝔰 p ≤ s J - C7_6_3 a n := by
…
```
Mentions: 𝓘, TileStructure.Forest.𝔖₀, TileStructure.Forest.𝓙₆, 𝔠, 𝔰, c, s
lemma TileStructure.Forest.thin_scale_impact' Lemma 7.6.3 with a floor on the constant to avoid casting line 230 source
Source documentation
Lemma 7.6.3 with a floor on the constant to avoid casting.

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, Ne and 19 more
Proof uses: Eq.mpr, id, Eq, congrArg, Eq.symm, propext, Int.cast_le, Int.cast_sub, LE.le.trans, TileStructure.Forest.thin_scale_impact, sub_le_sub_left, Int.floor_le
119 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma thin_scale_impact' (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (hu : u₁ ≠ u₂)
    (h2u : 𝓘 u₁ ≤ 𝓘 u₂) (hp : p ∈ t u₂ \ 𝔖₀ t u₁ u₂) (hJ : J ∈ 𝓙₆ t u₁)
    (hd : ¬Disjoint (ball (𝔠 p) (8 * D ^ 𝔰 p)) (ball (c J) (8 * D ^ s J))) :
    𝔰 p ≤ s J - ⌊C7_6_3 a n⌋ := by
…
```
Mentions: 𝓘, TileStructure.Forest.𝔖₀, TileStructure.Forest.𝓙₆, 𝔠, 𝔰, c, s
lemma TileStructure.Forest.square_function_count Lemma 7.6.4 line 243 source
Source documentation
Lemma 7.6.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 23 more
Proof uses: LT.lt, HAdd.hAdd, Or, lt_or_ge, Finset, EmptyCollection.emptyCollection, Eq.mpr, id, Eq.trans, forall_congr, True, implies_congr, Eq.refl, true_implies, Neg.neg, And.left, GridStructure.s, GridStructure.range_s_subset, Exists.intro, GridStructure.Grid and 292 more
447 instances, coercions and auxiliary constants left out.

Tactic trace: 138 steps
Open to load the checked before-and-after goal states.
```
lemma square_function_count (hJ : J ∈ 𝓙₆ t u₁) {s' : ℤ} :
    ⨍⁻ x in J, (∑ I with s I = s J - s' ∧ Disjoint (I : Set X) (𝓘 u₁) ∧
    ¬Disjoint (J : Set X) (ball (c I) (8 * D ^ s I)),
    (ball (c I) (8 * D ^ s I)).indicator 1 x) ^ 2 ∂volume ≤ C7_6_4 a s' := by
…
```
Mentions: TileStructure.Forest.𝓙₆, s, 𝓘, c
lemma TileStructure.Forest.sum_𝓙₆_indicator_sq_eq line 371 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, 𝔓, Grid, ENNReal, Eq and 8 more
Proof uses: Eq.mpr, HMul.hMul, id, congrArg, sq, Finset.sum_mul_sum, Prod, SProd.sprod, Finset, Prod.fst, Prod.snd, Eq.symm, Finset.sum_product', LE.le, Finset.diag, Finset.filter, Finset.diag_eq_filter, Finset.filter_subset, Finset.sum_subset, Not and 25 more
87 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
lemma TileStructure.Forest.btp_expansion line 387 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, Eq and 22 more
Proof uses: LT.lt, volume_coeGrid_pos, defaultD_pos, Top.top, volume_coeGrid_lt_top, Trans.trans, MeasureTheory.laverage, MeasureTheory.average, Set.indicator, id, Eq.mpr, Finset.filter, Finset.univ, congr, congrArg, congrFun', autoParam, funext, Finset.sum_congr, Eq.refl and 87 more
252 instances, coercions and auxiliary constants left out.

Tactic trace: 32 steps
Open to load the checked before-and-after goal states.
lemma TileStructure.Forest.e763 Equation (7.6.3) of Lemma 7.6.2 line 428 source
Source documentation
Equation (7.6.3) of Lemma 7.6.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, 𝔓, Membership.mem, Ne, LE.le and 38 more
Proof uses: Trans.trans, Neg.neg, HDiv.hDiv, TileStructure.Forest.btp_expansion, eq_of_heq, outParam, HPow, HEq, Eq.refl, HEq.refl, Eq.symm, Finset.sum_congr, Finset, HMul, MeasureTheory.setLIntegral_congr_fun, GridStructure.coeGrid_measurable, id, ENorm, Eq.rec, Finset.univ and 83 more
309 instances, coercions and auxiliary constants left out.

Tactic trace: 49 steps
Open to load the checked before-and-after goal states.
```
lemma e763 (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (hu : u₁ ≠ u₂) (h2u : 𝓘 u₁ ≤ 𝓘 u₂)
    (hf : BoundedCompactSupport f) :
    eLpNorm (approxOnCube (𝓙₆ t u₁) (‖adjointCarlesonSum (t u₂ \ 𝔖₀ t u₁ u₂) f ·‖)) 2 volume ≤
    ∑ k ∈ Finset.Icc ⌊C7_6_3 a n⌋ (2 * S),
    (∑ J ∈ (𝓙₆ t u₁).toFinset, (volume (J : Set X))⁻¹ *
    (∫⁻ y in J, ∑ p ∈ (t u₂ \ 𝔖₀ t u₁ u₂).toFinset with
      ¬Disjoint ↑J (ball (𝔠 p) (8 * D ^ 𝔰 p)) ∧ 𝔰 p = s J - k,
    ‖adjointCarleson p f y‖ₑ) ^ 2) ^ (2 : ℝ)⁻¹ := by
…
```
Mentions: 𝓘, TileStructure.Forest.approxOnCube, TileStructure.Forest.𝓙₆, adjointCarlesonSum, TileStructure.Forest.𝔖₀, k, 𝔠, 𝔰, s, adjointCarleson
lemma TileStructure.Forest.btp_integral_bound The critical bound on the integral in Equation (7.6.3) line 504 source
Source documentation
The critical bound on the integral in Equation (7.6.3). It holds for any cubes I, J.

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, LE.le, ENNReal and 33 more
Proof uses: Trans.trans, MeasureTheory.laverage, Inv.inv, MeasureTheory.Measure, Set.iUnion, Finset, E, MeasureTheory.lintegral_mono_fn', le_refl, Finset.sum_le_sum, TileStructure.Forest.enorm_adjointCarleson_le_mul_indicator, eq_of_heq, MeasurableSpace, HEq, Eq.refl, HEq.refl, Eq.symm, funext, Finset.sum_congr, Finset.ext and 114 more
249 instances, coercions and auxiliary constants left out.

Tactic trace: 53 steps
Open to load the checked before-and-after goal states.
```
lemma btp_integral_bound :
    ∫⁻ y in J, ∑ p ∈ (t u₂ \ 𝔖₀ t u₁ u₂).toFinset with
      ¬Disjoint ↑J (ball (𝔠 p) (8 * D ^ 𝔰 p)) ∧ 𝓘 p = I, ‖adjointCarleson p f y‖ₑ ≤
    C2_1_3 a * 2 ^ (4 * a) * ∫⁻ y in J, (ball (c I) (8 * D ^ s I)).indicator 1 y *
      maximalFunction volume 𝓑 c𝓑 r𝓑 1 f y := by
…
```
Mentions: TileStructure.Forest.𝔖₀, 𝔠, 𝔰, 𝓘, adjointCarleson, C2_1_3, c, s, TileStructure.Forest.𝓑, TileStructure.Forest.c𝓑, TileStructure.Forest.r𝓑
lemma TileStructure.Forest.e764_preCS Equation (7.6.4) of Lemma 7.6.2 (before applying Cauchy–Schwarz) line 565 source
Source documentation
Equation (7.6.4) of Lemma 7.6.2 (before applying Cauchy–Schwarz).

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 43 more
Proof uses: Trans.trans, 𝔠, 𝔰, ENorm.enorm, adjointCarleson, TileStructure.Forest.e763, Finset.sum_congr, Eq.refl, Finset, eq_of_heq, outParam, HPow, HEq, HEq.refl, Eq.symm, HMul, MeasurableSpace, funext, Eq.mpr, id and 68 more
292 instances, coercions and auxiliary constants left out.

Tactic trace: 31 steps
Open to load the checked before-and-after goal states.
```
lemma e764_preCS (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (hu : u₁ ≠ u₂) (h2u : 𝓘 u₁ ≤ 𝓘 u₂)
    (hf : BoundedCompactSupport f) :
    eLpNorm (approxOnCube (𝓙₆ t u₁) (‖adjointCarlesonSum (t u₂ \ 𝔖₀ t u₁ u₂) f ·‖)) 2 volume ≤
    C2_1_3 a * 2 ^ (4 * a) * ∑ k ∈ Finset.Icc ⌊C7_6_3 a n⌋ (2 * S),
    (∑ J ∈ (𝓙₆ t u₁).toFinset, (volume (J : Set X))⁻¹ *
    (∑ I with s I = s J - k ∧ Disjoint (I : Set X) (𝓘 u₁) ∧
      ¬Disjoint ↑J (ball (c I) (8 * D ^ s I)),
    ∫⁻ y in J, (ball (c I) (8 * D ^ s I)).indicator 1 y *
      maximalFunction volume 𝓑 c𝓑 r𝓑 1 f y) ^ 2) ^ (2 : ℝ)⁻¹ := by
…
```
Mentions: 𝓘, TileStructure.Forest.approxOnCube, TileStructure.Forest.𝓙₆, adjointCarlesonSum, TileStructure.Forest.𝔖₀, C2_1_3, k, s, c, TileStructure.Forest.𝓑, TileStructure.Forest.c𝓑, TileStructure.Forest.r𝓑
lemma TileStructure.Forest.e764_postCS Equation (7.6.4) of Lemma 7.6.2 (after applying Cauchy–Schwarz and simplification) line 629 source
Source documentation
Equation (7.6.4) of Lemma 7.6.2 (after applying Cauchy–Schwarz and simplification).

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 30 more
Proof uses: AEMeasurable, Measurable.aemeasurable, measurable_maximalFunction, Trans.trans, Eq, Set.toFinset, Classical.propDecidable, MeasureTheory.lintegral, MeasureTheory.Measure.restrict, Inv.inv, TileStructure.Forest.C7_6_4, MeasureTheory.laverage, Finset.filter, And, s, HSub.hSub, Disjoint, Not, Metric.ball, c and 147 more
329 instances, coercions and auxiliary constants left out.

Tactic trace: 55 steps
Open to load the checked before-and-after goal states.
```
lemma e764_postCS (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (hu : u₁ ≠ u₂) (h2u : 𝓘 u₁ ≤ 𝓘 u₂)
    (hf : BoundedCompactSupport f) :
    eLpNorm (approxOnCube (𝓙₆ t u₁) (‖adjointCarlesonSum (t u₂ \ 𝔖₀ t u₁ u₂) f ·‖)) 2 volume ≤
    C2_1_3 a * 2 ^ (11 * a + 2) *
    (∑ k ∈ Finset.Icc ⌊C7_6_3 a n⌋ (2 * S), (D : ℝ≥0∞) ^ (-k * κ / 2)) *
    eLpNorm ((𝓘 u₁ : Set X).indicator (maximalFunction volume 𝓑 c𝓑 r𝓑 1 f ·)) 2 volume := by
…
```
Mentions: 𝓘, TileStructure.Forest.approxOnCube, TileStructure.Forest.𝓙₆, adjointCarlesonSum, TileStructure.Forest.𝔖₀, C2_1_3, k, TileStructure.Forest.𝓑, TileStructure.Forest.c𝓑, TileStructure.Forest.r𝓑
lemma TileStructure.Forest.btp_constant_bound line 704 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, LE.le, ENNReal, HMul.hMul, C2_1_3, HPow.hPow, OfNat.ofNat, HAdd.hAdd, Finset.sum, Finset.Icc, Int.floor, TileStructure.Forest.C7_6_3, defaultS, defaultD and 4 more
Proof uses: Trans.trans, Eq, HSub.hSub, 𝕔, defaultZ, Finset.range, Int.toNat, Eq.mpr, id, Eq.rec, Eq.refl, Eq.trans, congrArg, mul_assoc, Finset.mul_sum, HMul, LT.lt, Or, Finset.Ico, le_or_gt and 243 more
332 instances, coercions and auxiliary constants left out.

Tactic trace: 77 steps
Open to load the checked before-and-after goal states.
lemma TileStructure.Forest.bound_for_tree_projection Lemma 7.6.2 line 770 source
Source documentation
Lemma 7.6.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, 𝔓, Membership.mem, Ne, LE.le and 22 more
Proof uses: LE.le.trans, C2_1_3, HPow.hPow, HAdd.hAdd, Finset.sum, Finset.Icc, Int.floor, TileStructure.Forest.C7_6_3, HDiv.hDiv, Neg.neg, TileStructure.Forest.e764_postCS, mul_le_mul_left, TileStructure.Forest.btp_constant_bound
154 instances, coercions and auxiliary constants left out.
```
lemma bound_for_tree_projection (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (hu : u₁ ≠ u₂) (h2u : 𝓘 u₁ ≤ 𝓘 u₂)
    (hf : BoundedCompactSupport f) :
    eLpNorm (approxOnCube (𝓙₆ t u₁) (‖adjointCarlesonSum (t u₂ \ 𝔖₀ t u₁ u₂) f ·‖)) 2 volume ≤
    C7_6_2 a n * eLpNorm ((𝓘 u₁ : Set X).indicator (maximalFunction volume 𝓑 c𝓑 r𝓑 1 f ·)) 2 volume :=
…
```
Mentions: 𝓘, TileStructure.Forest.approxOnCube, TileStructure.Forest.𝓙₆, adjointCarlesonSum, TileStructure.Forest.𝔖₀, TileStructure.Forest.𝓑, TileStructure.Forest.c𝓑, TileStructure.Forest.r𝓑
lemma TileStructure.Forest.cntp_approxOnCube_eq line 776 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, TileStructure.Forest.approxOnCube and 9 more
Proof uses: Eq.mpr, id, congrArg, rfl, funext, Finset.sum, Grid, Finset.filter, Classical.propDecidable, Finset.univ, MeasureTheory.average, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, congr, Finset.sum_congr, Eq.refl, Finset, Trans.trans, Eq.symm, Finset.sum_subset and 63 more
107 instances, coercions and auxiliary constants left out.

Tactic trace: 33 steps
Open to load the checked before-and-after goal states.
lemma TileStructure.Forest.correlation_near_tree_parts Lemma 7.4.6 line 820 source
Source documentation
Lemma 7.4.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, 𝔓, Membership.mem, Ne, LE.le and 19 more
Proof uses: Eq.mpr, id, Eq, congrArg, rfl, Trans.trans, TileStructure.Forest.C7_2_1, TileStructure.Forest.C7_6_2, maximalFunction, Prod, TileStructure.Forest.𝓑, TileStructure.Forest.c𝓑, TileStructure.Forest.r𝓑, TileStructure.Forest.approxOnCube, TileStructure.Forest.𝓙, Norm.norm, TileStructure.Forest.𝓛, carlesonSum, Eq.symm, RCLike.enorm_conj and 49 more
208 instances, coercions and auxiliary constants left out.

Tactic trace: 28 steps
Open to load the checked before-and-after goal states.
```
lemma correlation_near_tree_parts (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (hu : u₁ ≠ u₂) (h2u : 𝓘 u₁ ≤ 𝓘 u₂)
    (hf₁ : BoundedCompactSupport f₁) (hf₂ : BoundedCompactSupport f₂) :
    ‖∫ x, adjointCarlesonSum (t u₁) f₁ x * conj (adjointCarlesonSum (t u₂ \ 𝔖₀ t u₁ u₂) f₂ x)‖ₑ ≤
    C7_4_6 a n *
    eLpNorm ((𝓘 u₁ : Set X).indicator (adjointBoundaryOperator t u₁ f₁) ·) 2 volume *
    eLpNorm ((𝓘 u₁ : Set X).indicator (adjointBoundaryOperator t u₂ f₂) ·) 2 volume := by
…
```
Mentions: 𝓘, adjointCarlesonSum, TileStructure.Forest.𝔖₀, TileStructure.Forest.adjointBoundaryOperator