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

58 declarations, 0 contain sorry, 0 declared as axioms

Section 5.3

Imports (5)

Imported by 2 files

lemma ordConnected_tilesAt Lemma 5.3.4 line 26 source
Source documentation
Lemma 5.3.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, Set.OrdConnected, 𝔓, TilesAt
Proof uses: Eq.mpr, Membership.mem, LE.le, Set.Icc, id, Eq, congrArg, propext, Set.ordConnected_def, Set.preimage, Grid, 𝓘, 𝓒, SDiff.sdiff, aux𝓒, HAdd.hAdd, OfNat.ofNat, And, Not, Set.ofPred and 27 more
80 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
lemma ordConnected_tilesAt : OrdConnected (TilesAt k : Set (𝔓 X)) := by
…
```
Mentions: TilesAt, k, 𝔓
lemma ordConnected_C Lemma 5.3.5 line 36 source
Source documentation
Lemma 5.3.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, Set.OrdConnected, 𝔓, ℭ
Proof uses: Eq.mpr, Membership.mem, LE.le, Set.Icc, id, Eq, congrArg, propext, Set.ordConnected_def, Set.ofPred, And, TilesAt, ENNReal, Set.Ioc, HPow.hPow, OfNat.ofNat, HSub.hSub, HMul.hMul, HAdd.hAdd, dens' and 52 more
112 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
```
lemma ordConnected_C : OrdConnected (ℭ k n : Set (𝔓 X)) := by
…
```
Mentions: ℭ, k, 𝔓
lemma ordConnected_C1 Lemma 5.3.6 line 48 source
Source documentation
Lemma 5.3.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, Set.OrdConnected, 𝔓, ℭ₁
Proof uses: Eq.mpr, Membership.mem, LE.le, Set.Icc, id, Eq, congrArg, propext, Set.ordConnected_def, ℭ, Set.mem_of_mem_of_subset, Set.OrdConnected.out, ordConnected_C, ℭ₁_subset_ℭ, SDiff.sdiff, preℭ₁, HAdd.hAdd, OfNat.ofNat, And, Not and 45 more
91 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
```
lemma ordConnected_C1 : OrdConnected (ℭ₁ k n j : Set (𝔓 X)) := by
…
```
Mentions: ℭ₁, k, 𝔓
lemma ordConnected_C2 Lemma 5.3.7 line 68 source
Source documentation
Lemma 5.3.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, Set.OrdConnected, 𝔓, ℭ₂
Proof uses: Eq.mpr, Membership.mem, LE.le, Set.Icc, id, Eq, congrArg, propext, Set.ordConnected_def, ℭ₁, Set.mem_of_mem_of_subset, ℭ₂_subset_ℭ₁, Set.OrdConnected.out, ordConnected_C1, dite, Classical.propDecidable, Eq.mp, Not, Set.layersAbove, HMul.hMul and 31 more
44 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
```
lemma ordConnected_C2 : OrdConnected (ℭ₂ k n j : Set (𝔓 X)) := by
…
```
Mentions: ℭ₂, k, 𝔓
lemma ordConnected_C3 Lemma 5.3.8 line 84 source
Source documentation
Lemma 5.3.8

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.OrdConnected, 𝔓, ℭ₃
Proof uses: Eq.mpr, Membership.mem, LE.le, Set.Icc, id, Eq, congrArg, propext, Set.ordConnected_def, ℭ₂, Set.mem_of_mem_of_subset, ℭ₃_subset_ℭ₂, Set.OrdConnected.out, ordConnected_C2, And, Exists, 𝔘₁, Ne, Grid, 𝓘 and 37 more
84 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
lemma ordConnected_C3 : OrdConnected (ℭ₃ k n j : Set (𝔓 X)) := by
…
```
Mentions: ℭ₃, k, 𝔓
lemma ordConnected_C4 Lemma 5.3.9 line 95 source
Source documentation
Lemma 5.3.9

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.OrdConnected, 𝔓, ℭ₄
Proof uses: Eq.mpr, Membership.mem, LE.le, Set.Icc, id, Eq, congrArg, propext, Set.ordConnected_def, ℭ₃, Set.mem_of_mem_of_subset, ℭ₄_subset_ℭ₃, Set.OrdConnected.out, ordConnected_C3, dite, Classical.propDecidable, Eq.mp, Eq.symm, Not, Set.layersBelow and 36 more
51 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
```
lemma ordConnected_C4 : OrdConnected (ℭ₄ k n j : Set (𝔓 X)) := by
…
```
Mentions: ℭ₄, k, 𝔓
lemma ordConnected_C5 Lemma 5.3.10 line 111 source
Source documentation
Lemma 5.3.10

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.OrdConnected, 𝔓, ℭ₅
Proof uses: Eq.mpr, Membership.mem, LE.le, Set.Icc, id, Eq, congrArg, propext, Set.ordConnected_def, ℭ₄, Set.mem_of_mem_of_subset, ℭ₅_subset_ℭ₄, Set.OrdConnected.out, ordConnected_C4, SDiff.sdiff, 𝔏₄, And, Not, True, congrFun' and 23 more
56 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
lemma ordConnected_C5 : OrdConnected (ℭ₅ k n j : Set (𝔓 X)) := by
…
```
Mentions: ℭ₅, k, 𝔓
def ℭ₆ The subset ℭ₆(k, n, j) of ℭ₅(k, n, j), given above (5.4.1) line 123 source
Source documentation
The subset ℭ₆(k, n, j) of ℭ₅(k, n, j), given above (5.4.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, 𝔓
Proof uses: Set.ofPred, And, Membership.mem, ℭ₅, Not, LE.le, 𝓘, G'
30 instances, coercions and auxiliary constants left out.
```
def ℭ₆ (k n j : ℕ) : Set (𝔓 X) :=
…
```
Mentions: k, 𝔓
lemma ℭ₆_subset_ℭ₅ line 126 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, 𝔓, ℭ₆, ℭ₅
Proof uses: Set.sep_subset, Not, 𝓘, G'
30 instances, coercions and auxiliary constants left out.
lemma ℭ₆_subset_ℭ line 127 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, 𝔓, ℭ₆, ℭ
Proof uses: LE.le.trans, ℭ₅, ℭ₆_subset_ℭ₅, ℭ₅_subset_ℭ
33 instances, coercions and auxiliary constants left out.
def 𝔗₁ The subset 𝔗₁(u) of ℭ₁(k, n, j), given in (5.4.1) line 131 source
Source documentation
The subset 𝔗₁(u) of ℭ₁(k, n, j), given in (5.4.1). In lemmas, we will assume u ∈ 𝔘₁ k n l

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, 𝔓
Proof uses: Set.ofPred, And, Membership.mem, ℭ₁, Ne, Grid, 𝓘, LE.le, TileLike, smul, OfNat.ofNat
36 instances, coercions and auxiliary constants left out.
```
def 𝔗₁ (k n j : ℕ) (u : 𝔓 X) : Set (𝔓 X) :=
…
```
Mentions: k, 𝔓
lemma 𝓘_lt_of_mem_𝔗₁ line 134 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, 𝔗₁, LT.lt, Grid and 1 more
Proof uses: lt_of_le_of_ne, And.left, LE.le, Prod.fst, OrderDual, FunctionDistances.Θ, smul, OfNat.ofNat, Prod.snd, And.right, Ne, TileLike, ℭ₁, And, Eq.mp, Set.ofPred, congrArg, propext, Set.mem_ofPred, 𝔗₁.eq_1
52 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
def 𝔘₂ The subset 𝔘₂(k, n, j) of 𝔘₁(k, n, j), given in (5.4.2) line 138 source
Source documentation
The subset 𝔘₂(k, n, j) of 𝔘₁(k, n, j), given in (5.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, 𝔓
Proof uses: Set.ofPred, And, Membership.mem, 𝔘₁, Not, Disjoint, 𝔗₁, ℭ₆
36 instances, coercions and auxiliary constants left out.
```
def 𝔘₂ (k n j : ℕ) : Set (𝔓 X) :=
…
```
Mentions: k, 𝔓
lemma 𝔘₂_subset_𝔘₁ line 141 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, 𝔓, 𝔘₂, 𝔘₁
Proof uses: Membership.mem, And.left, Not, Disjoint, 𝔗₁, ℭ₆
37 instances, coercions and auxiliary constants left out.
def URel The relation ∼ defined below (5.4.2) line 144 source
Source documentation
The relation ∼ defined below (5.4.2). It is an equivalence relation on 𝔘₂ k n 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, 𝔓
Proof uses: Or, Eq, Exists, And, Membership.mem, 𝔗₁, LE.le, TileLike, smul, OfNat.ofNat
35 instances, coercions and auxiliary constants left out.
```
def URel (k n j : ℕ) (u u' : 𝔓 X) : Prop :=
…
```
Mentions: k, 𝔓
lemma URel.rfl line 147 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, 𝔓, URel
Proof uses: Or.inl, Eq, Exists, And, Membership.mem, 𝔗₁, LE.le, TileLike, smul, OfNat.ofNat, rfl
35 instances, coercions and auxiliary constants left out.
lemma URel.not_disjoint Lemma 5.4.1, part 2 line 151 source
Source documentation
Lemma 5.4.1, part 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, 𝔓, Membership.mem, 𝔘₂, URel, Not and 9 more
Proof uses: dite, Eq, Classical.propDecidable, Eq.mpr, id, congrArg, Iff.mpr, Exists, And, Set.not_disjoint_iff, Exists.intro, And.intro, Metric.mem_ball_self, Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Bool, Nat.ble, 𝔗₁ and 75 more
179 instances, coercions and auxiliary constants left out.

Tactic trace: 48 steps
Open to load the checked before-and-after goal states.
```
lemma URel.not_disjoint (hu : u ∈ 𝔘₂ k n j) (hu' : u' ∈ 𝔘₂ k n j) (huu' : URel k n j u u') :
    ¬Disjoint (ball_(u) (𝒬 u) 100) (ball_(u') (𝒬 u') 100) := by
…
```
Mentions: 𝔘₂, k, URel
lemma URel.eq Lemma 5.4.1, part 1 line 197 source
Source documentation
Lemma 5.4.1, part 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, 𝔓, Membership.mem, 𝔘₂, URel, Eq and 2 more
Proof uses: dite, Classical.propDecidable, Eq.mpr, id, congrArg, Eq.refl, Not, Disjoint, WithFunctionDistance, 𝔠, HDiv.hDiv, HPow.hPow, 𝔰, OfNat.ofNat, Metric.ball, PreTileStructure.𝒬, URel.not_disjoint, LT.lt, Function.mt, And.right and 30 more
78 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
```
lemma URel.eq (hu : u ∈ 𝔘₂ k n j) (hu' : u' ∈ 𝔘₂ k n j) (huu' : URel k n j u u') : 𝓘 u = 𝓘 u' := by
…
```
Mentions: 𝔘₂, k, URel, 𝓘
lemma urel_of_not_disjoint Helper for 5.4.2 that is also used in 5.4.9 line 210 source
Source documentation
Helper for 5.4.2 that is also used in 5.4.9.

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, 𝔘₂, Eq, Grid and 12 more
Proof uses: And, Exists, Eq.mp, congrArg, propext, Set.not_disjoint_iff, 𝔗₁, ℭ₆, And.right, 𝔘₁, Set.ofPred, Set.mem_ofPred, 𝔘₂.eq_1, LE.le, Trans.trans, LT.lt, Dist.dist, HAdd.hAdd, dist_triangle, add_le_add and 37 more
137 instances, coercions and auxiliary constants left out.

Tactic trace: 26 steps
Open to load the checked before-and-after goal states.
```
lemma urel_of_not_disjoint {x y : 𝔓 X} (my : y ∈ 𝔘₂ k n j) (xye : 𝓘 x = 𝓘 y)
    (nd : ¬Disjoint (ball_(x) (𝒬 x) 100) (ball_(y) (𝒬 y) 100)) : URel k n j y x := by
…
```
Mentions: 𝔓, 𝔘₂, k, 𝓘, URel
lemma equivalenceOn_urel Lemma 5.4.2 line 238 source
Source documentation
Lemma 5.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, EquivalenceOn, 𝔓, URel, 𝔘₂
Proof uses: EquivalenceOn.mk, Membership.mem, URel.rfl, urel_of_not_disjoint, URel.eq, URel.not_disjoint, dite, Eq, Classical.propDecidable, Eq.mpr, id, congrArg, Not, Grid, 𝓘, Disjoint, WithFunctionDistance, 𝔠, HDiv.hDiv, HPow.hPow and 59 more
113 instances, coercions and auxiliary constants left out.

Tactic trace: 44 steps
Open to load the checked before-and-after goal states.
```
lemma equivalenceOn_urel : EquivalenceOn (URel (X := X) k n j) (𝔘₂ k n j) where
…
```
Mentions: EquivalenceOn, URel, k, 𝔘₂
def 𝔘₃ 𝔘₃(k, n, j) ⊆ 𝔘₂ k n j is an arbitary set of representatives of URel on 𝔘₂ k n j, given above (5.4.5) line 285 source
Source documentation
𝔘₃(k, n, j) ⊆ 𝔘₂ k n j is an arbitary set of representatives of URel on 𝔘₂ k n j, given above (5.4.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, 𝔓
Proof uses: EquivalenceOn.reprs, URel, 𝔘₂, equivalenceOn_urel
26 instances, coercions and auxiliary constants left out.
```
def 𝔘₃ (k n j : ℕ) : Set (𝔓 X) :=
…
```
Mentions: k, 𝔓
lemma 𝔘₃_subset_𝔘₂ line 288 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, 𝔓, 𝔘₃, 𝔘₂
Proof uses: EquivalenceOn.reprs_subset, URel, equivalenceOn_urel
27 instances, coercions and auxiliary constants left out.
def 𝔗₂ The subset 𝔗₂(u) of ℭ₆(k, n, j), given in (5.4.5) line 292 source
Source documentation
The subset 𝔗₂(u) of ℭ₆(k, n, j), given in (5.4.5). In lemmas, we will assume u ∈ 𝔘₃ k n l

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, 𝔓
Proof uses: Inter.inter, ℭ₆, Set.iUnion, Membership.mem, 𝔘₂, URel, 𝔗₁
28 instances, coercions and auxiliary constants left out.
```
def 𝔗₂ (k n j : ℕ) (u : 𝔓 X) : Set (𝔓 X) :=
…
```
Mentions: k, 𝔓
lemma 𝔗₂_subset_ℭ₆ line 295 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, 𝔗₂, ℭ₆
Proof uses: Set.inter_subset_left, Set.iUnion, Membership.mem, 𝔘₂, URel, 𝔗₁
28 instances, coercions and auxiliary constants left out.
lemma C6_forest Lemma 5.4.3 line 298 source
Source documentation
Lemma 5.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, Eq, 𝔓, ℭ₆, Set.iUnion, Membership.mem and 2 more
Proof uses: Set.ext, Iff.intro, ℭ₃, LE.le.trans, ℭ₄, ℭ₅, ℭ₆_subset_ℭ₅, ℭ₅_subset_ℭ₄, ℭ₄_subset_ℭ₃, ℭ₂, And.left, Not, And, Exists, 𝔘₁, Ne, Grid, 𝓘, LE.le, TileLike and 39 more
57 instances, coercions and auxiliary constants left out.

Tactic trace: 27 steps
Open to load the checked before-and-after goal states.
```
lemma C6_forest : ℭ₆ (X := X) k n j = ⋃ u ∈ 𝔘₃ k n j, 𝔗₂ k n j u := by
…
```
Mentions: ℭ₆, k, 𝔘₃, 𝔗₂
lemma forest_disjoint This one could deserve a lemma in the blueprint, as it is needed to decompose the sum of Carleson operators over disjoint subfamilies line 316 source
Source documentation
This one could deserve a lemma in the blueprint, as it is needed to decompose the sum of Carleson operators over disjoint subfamilies.

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, 𝔓, 𝔘₃, 𝔗₂
Proof uses: Membership.mem, Ne, id, Function.onFun, Disjoint, Iff.mpr, Not, Set.disjoint_left, And, 𝔘₂, URel, 𝔗₁, Exists, Eq, And.right, ℭ₆, Eq.mp, Eq.trans, Inter.inter, Set.iUnion and 28 more
74 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
```
lemma forest_disjoint : (𝔘₃ k n j).PairwiseDisjoint (fun u ↦ 𝔗₂ (X := X) k n j u) := by
…
```
Mentions: 𝔘₃, k, 𝔗₂
lemma forest_geometry Lemma 5.4.4, verifying (2.0.32) line 334 source
Source documentation
Lemma 5.4.4, verifying (2.0.32)

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, 𝔘₃, 𝔗₂, LE.le and 3 more
Proof uses: ℭ₆, Exists, 𝔘₂, Set.iUnion, URel, 𝔗₁, And, Eq.mp, congrArg, propext, Set.mem_iUnion₂, Inter.inter, Set.mem_inter_iff, 𝔗₂.eq_1, Set.mem_iUnion, ℭ₁, Ne, Grid, 𝓘, Set.ofPred and 49 more
125 instances, coercions and auxiliary constants left out.

Tactic trace: 28 steps
Open to load the checked before-and-after goal states.
```
lemma forest_geometry (hu : u ∈ 𝔘₃ k n j) (hp : p ∈ 𝔗₂ k n j u) : smul 4 p ≤ smul 1 u := by
…
```
Mentions: 𝔘₃, k, 𝔗₂, smul
lemma forest_convex Lemma 5.4.5, verifying (2.0.33) line 360 source
Source documentation
Lemma 5.4.5, verifying (2.0.33)

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.OrdConnected, 𝔗₂
Proof uses: Eq.mpr, Membership.mem, LE.le, Set.Icc, id, Eq, congrArg, propext, Set.ordConnected_def, ℭ₅, Set.OrdConnected.out, ordConnected_C5, LE.le.trans, ℭ₆, 𝔗₂_subset_ℭ₆, ℭ₆_subset_ℭ₅, Set.ofPred, And, Not, 𝓘 and 67 more
96 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
```
lemma forest_convex : OrdConnected (𝔗₂ k n j u) := by
…
```
Mentions: 𝔗₂, k
lemma forest_separation Lemma 5.4.6, verifying (2.0.36) Note: swapped u and u' to match (2.0.36) line 379 source
Source documentation
Lemma 5.4.6, verifying (2.0.36) Note: swapped u and u' to match (2.0.36)

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, 𝔘₃, Ne, 𝔗₂ and 15 more
Proof uses: ℭ₆, Exists, 𝔘₂, URel, 𝔗₁, And, Eq.mp, Set.iUnion, congrArg, funext, propext, exists_prop_congr, Iff.of_eq, Eq.refl, Inter.inter, ℭ₁, TileLike, smul, Set.minLayer, exists_scale_add_le_of_mem_layersAbove and 190 more
294 instances, coercions and auxiliary constants left out.

Tactic trace: 71 steps
Open to load the checked before-and-after goal states.
```
lemma forest_separation (hu : u ∈ 𝔘₃ k n j) (hu' : u' ∈ 𝔘₃ k n j) (huu' : u ≠ u')
    (hp : p ∈ 𝔗₂ k n j u') (h : 𝓘 p ≤ 𝓘 u) : 2 ^ (Z * (n + 1)) < dist_(p) (𝒬 p) (𝒬 u) := by
…
```
Mentions: 𝔘₃, k, 𝔗₂, 𝓘
lemma forest_inner Lemma 5.4.7, verifying (2.0.37) line 438 source
Source documentation
Lemma 5.4.7, verifying (2.0.37)

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, 𝔘₃, 𝔗₂, LE.le and 7 more
Proof uses: ℭ₄, LE.le.trans, ℭ₅, ℭ₆, 𝔗₂_subset_ℭ₆, ℭ₆_subset_ℭ₅, ℭ₅_subset_ℭ₄, ℭ₁, ℭ₂, ℭ₃, ℭ₄_subset_ℭ₃, ℭ₃_subset_ℭ₂, ℭ₂_subset_ℭ₁, And, Set.maxLayer, HAdd.hAdd, defaultZ, Exists, exists_le_add_scale_of_mem_layersBelow, 𝔘₁ and 179 more
206 instances, coercions and auxiliary constants left out.

Tactic trace: 64 steps
Open to load the checked before-and-after goal states.
```
lemma forest_inner (hu : u ∈ 𝔘₃ k n j) (hp : p ∈ 𝔗₂ k n j u) :
    ball (𝔠 p) (8 * D ^ 𝔰 p) ⊆ 𝓘 u := by
…
```
Mentions: 𝔘₃, k, 𝔗₂, 𝔠, 𝔰, 𝓘
def C5_4_8 The multiplicity appearing in Lemma 5.4.8 line 490 source
Source documentation
The multiplicity appearing in Lemma 5.4.8.

standard axioms: propext what this means
Statement uses: Nat
Proof uses: HMul.hMul, HAdd.hAdd, OfNat.ofNat, HPow.hPow
9 instances, coercions and auxiliary constants left out.
```
def C5_4_8 (n : ℕ) : ℕ := (4 * n + 12) * 2 ^ n
```
lemma exists_smul_le_of_𝔘₃ line 492 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, 𝔓, 𝔘₃, Exists, 𝔐, LE.le and 4 more
Proof uses: ℭ₁, LE.le.trans, 𝔘₁, 𝔘₂, 𝔘₃_subset_𝔘₂, 𝔘₂_subset_𝔘₁, 𝔘₁_subset_ℭ₁, LT.lt, Finset.card, Set.toFinset, 𝔅, Classical.propDecidable, LT.lt.trans_le, HPow.hPow, pow_pos, Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Nat.ble and 26 more
87 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
def mf The good choice of an element to get a contradiction in the proof of Lemma 5.4.8 line 503 source
Source documentation
The good choice of an element to get a contradiction in the proof of Lemma 5.4.8.

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, 𝔓, 𝔘₃, 𝔐
Proof uses: Exists.choose, LE.le, TileLike, smul, OfNat.ofNat, Membership.mem, exists_smul_le_of_𝔘₃
38 instances, coercions and auxiliary constants left out.
```
def mf (u : 𝔘₃ (X := X) k n j) : 𝔐 (X := X) k n := (exists_smul_le_of_𝔘₃ u).choose
…
```
Mentions: 𝔘₃, k, 𝔐, exists_smul_le_of_𝔘₃
lemma mf_injOn line 506 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.InjOn, 𝔓, 𝔘₃, 𝔐, mf and 4 more
Proof uses: Eq, LE.le, TileLike, smul, OfNat.ofNat, Exists.choose_spec, exists_smul_le_of_𝔘₃, Eq.rec, Eq.symm, Eq.mp, congrArg, rfl, WithFunctionDistance, c, HDiv.hDiv, HPow.hPow, s, Metric.ball, PreTileStructure.𝒬, And.right and 48 more
99 instances, coercions and auxiliary constants left out.

Tactic trace: 27 steps
Open to load the checked before-and-after goal states.
lemma stackSize_𝔘₃_le_𝔐 line 530 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, stackSize, 𝔘₃, 𝔐
Proof uses: 𝔓, dite, Membership.mem, Classical.propDecidable, mf, Subtype.mk, Not, Inhabited.default, id, Eq.mpr, Finset.sum, Finset.filter, Finset.univ, Set.indicator, 𝓘, OfNat.ofNat, ite, Eq, congr, congrArg and 42 more
72 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
lemma forest_stacking Lemma 5.4.8, used to verify that 𝔘₄ satisfies 2.0.34 line 544 source
Source documentation
Lemma 5.4.8, used to verify that 𝔘₄ satisfies 2.0.34.

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, stackSize, 𝔘₃, C5_4_8
Proof uses: Decidable.byContradiction, Not, Finset, 𝔓, Finset.filter, And, Membership.mem, Grid, 𝓘, Classical.propDecidable, Finset.univ, Eq, Finset.card, id, Eq.mpr, Finset.sum, Set.indicator, OfNat.ofNat, ite, congrArg and 111 more
120 instances, coercions and auxiliary constants left out.

Tactic trace: 35 steps
Open to load the checked before-and-after goal states.
```
lemma forest_stacking (x : X) (hkn : k ≤ n) : stackSize (𝔘₃ (X := X) k n j) x ≤ C5_4_8 n := by
…
```
Mentions: k, stackSize, 𝔘₃, C5_4_8
def 𝔘₄ Define 𝔘₄ k n j l as the union of 2 ^ n disjoint subfamilies in 𝔘₃ k n j, to make sure the multiplicity is at most 2 ^ n to get a forest line 586 source
Source documentation
Define 𝔘₄ k n j l as the union of 2 ^ n disjoint subfamilies in 𝔘₃ k n j, to make sure the multiplicity is at most 2 ^ n to get a forest.

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, 𝔓
Proof uses: Set.iUnion, Membership.mem, Set.Ico, HMul.hMul, HPow.hPow, OfNat.ofNat, HAdd.hAdd, iteratedMaximalSubfamily, 𝔘₃
37 instances, coercions and auxiliary constants left out.
```
def 𝔘₄ (k n j l : ℕ) : Set (𝔓 X) :=
…
```
Mentions: k, 𝔓
lemma 𝔘₄_subset_𝔘₃ line 589 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, 𝔓, 𝔘₄, 𝔘₃
Proof uses: of_eq_true, Eq.trans, Set.iUnion, And, HMul.hMul, HPow.hPow, OfNat.ofNat, LT.lt, HAdd.hAdd, iteratedMaximalSubfamily, True, congrFun', congrArg, Membership.mem, Set.Ico, funext, Set.iUnion_congr_Prop, Iff.of_eq, Eq.refl, forall_congr and 2 more
44 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma iUnion_𝔘₄ The sets (𝔘₄(k, n, j, l))_l form a partition of 𝔘₃ k n j line 594 source
Source documentation
The sets (𝔘₄(k, n, j, l))_l form a partition of 𝔘₃ k n 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, LE.le, Eq, 𝔓, Set.iUnion, Membership.mem and 6 more
Proof uses: LT.lt, HPow.hPow, iteratedMaximalSubfamily, Set.Subset.antisymm, Eq.mpr, id, Eq.trans, congrFun', congrArg, funext, And, Set.Ico, Set.iUnion_congr_Prop, Iff.of_eq, Eq.refl, Set.biUnion_and', forall_congr, implies_congr, Set.subset_biUnion_of_mem, Nat.le and 16 more
83 instances, coercions and auxiliary constants left out.

Tactic trace: 28 steps
Open to load the checked before-and-after goal states.
```
lemma iUnion_𝔘₄ (hkn : k ≤ n) : ⋃ l ∈ Iio (4 * n + 12), 𝔘₄ (X := X) k n j l = 𝔘₃ k n j := by
…
```
Mentions: k, 𝔘₄, 𝔘₃
lemma C6_forest' line 623 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, Eq, 𝔓, ℭ₆, Set.iUnion and 7 more
Proof uses: Eq.mpr, 𝔘₃, id, congrArg, C6_forest, Eq.symm, iUnion_𝔘₄, of_eq_true, Eq.trans, LT.lt, True, congr, And, funext, Exists, Set.iUnion_congr_Prop, Iff.of_eq, congrFun', Eq.refl, Set.iUnion_exists and 2 more
46 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma pairwiseDisjoint_𝔘₄ line 628 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, 𝔓, Set.univ, 𝔘₄
Proof uses: Membership.mem, Ne, Iff.mpr, Disjoint, Set.disjoint_iff_forall_ne, And, LE.le, HMul.hMul, HPow.hPow, OfNat.ofNat, LT.lt, HAdd.hAdd, iteratedMaximalSubfamily, 𝔘₃, Exists, Eq.mp, Eq.trans, Set.iUnion, congrFun', congrArg and 17 more
75 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
lemma stackSize_𝔘₄_le line 642 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, stackSize, 𝔘₄, HPow.hPow, OfNat.ofNat
Proof uses: Trans.trans, Eq, Finset.sum, Finset.Ico, HMul.hMul, HAdd.hAdd, iteratedMaximalSubfamily, 𝔘₃, rfl, Eq.mpr, 𝔓, Finset.filter, Membership.mem, Set.iUnion, Set.Ico, Classical.propDecidable, Finset.univ, Set.indicator, 𝓘, id and 50 more
114 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
def forest The forest based on 𝔘₄ k n j l line 668 source
Source documentation
The forest based on 𝔘₄ k n j l.

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: TileStructure.Forest.mk, 𝔘₄, 𝔗₂, 𝔓, Membership.mem, forest_convex, stackSize_𝔘₄_le
32 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
```
def forest : Forest X n where
…
```
lemma carlesonSum_𝔓₁_eq_sum From the fact that the ℭ₅ k n j are disjoint, one can rewrite the whole Carleson sum over 𝔓₁ (the union of the ℭ₅ k n j) as a sum of Carleson sums over the ℭ₅ k n j line 699 source
Source documentation
From the fact that the ℭ₅ k n j are disjoint, one can rewrite the whole Carleson sum over 𝔓₁ (the union of the ℭ₅ k n j) as a sum of Carleson sums over the ℭ₅ k n 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, Eq, carlesonSum, 𝔓₁, Finset.sum, Finset.Iic and 5 more
Proof uses: Eq.mpr, Sigma, Finset.sigma, Sigma.fst, Sigma.snd, id, congrArg, Eq.trans, Finset.sum_congr, Eq.refl, Finset, Membership.mem, Finset.sum_sigma', Set.iUnion, 𝔓, sum_carlesonSum_of_pairwiseDisjoint, Ne, Function.onFun, Disjoint, Sigma.mk and 37 more
72 instances, coercions and auxiliary constants left out.

Tactic trace: 23 steps
Open to load the checked before-and-after goal states.
```
lemma carlesonSum_𝔓₁_eq_sum {f : X → ℂ} {x : X} :
    carlesonSum 𝔓₁ f x = ∑ n ≤ maxℭ X, ∑ k ≤ n, ∑ j ≤ 2 * n + 3, carlesonSum (ℭ₅ k n j) f x := by
…
```
Mentions: carlesonSum, 𝔓₁, maxℭ, k, ℭ₅
lemma carlesonSum_ℭ₅_eq_ℭ₆ The Carleson sum over ℭ₅ and ℭ₆ coincide, for points in G \ G' line 721 source
Source documentation
The Carleson sum over ℭ₅ and ℭ₆ coincide, for points in G \ G'.

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, SDiff.sdiff, G', Eq, carlesonSum and 2 more
Proof uses: id, Eq.symm, Finset.sum, 𝔓, Finset.filter, Classical.propDecidable, Finset.univ, carlesonOn, Finset.sum_subset, Finset, Eq.mpr, congrArg, propext, Finset.mem_filter_univ, ℭ₆_subset_ℭ₅, Eq.mp, Not, Grid, 𝓘, And.right and 32 more
78 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
```
lemma carlesonSum_ℭ₅_eq_ℭ₆ {f : X → ℂ} {x : X} (hx : x ∈ G \ G') {k n j : ℕ} :
    carlesonSum (ℭ₅ k n j) f x = carlesonSum (ℭ₆ k n j) f x := by
…
```
Mentions: G', k, carlesonSum, ℭ₅, ℭ₆
lemma carlesonSum_ℭ₆_eq_sum The Carleson sum over ℭ₆ can be decomposed as a sum over 4 n + 12 forests based on 𝔘₄ k n j l line 741 source
Source documentation
The Carleson sum over ℭ₆ can be decomposed as a sum over 4 n + 12 forests based on 𝔘₄ k n j l.

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, Eq, carlesonSum, ℭ₆, Finset.sum and 9 more
Proof uses: Eq.mpr, Finset, id, congrArg, sum_carlesonSum_of_pairwiseDisjoint, Ne, Function.onFun, Disjoint, Not, Eq.trans, forall_congr, And, Exists, implies_congr, funext, Eq.refl, pairwiseDisjoint_𝔘₄, Set.mem_univ, Iff.mp, Set.disjoint_iff_forall_ne and 18 more
78 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
```
lemma carlesonSum_ℭ₆_eq_sum {f : X → ℂ} {x : X} {k n j : ℕ} (hkn : k ≤ n) :
    carlesonSum (ℭ₆ k n j) f x =
      ∑ l < 4 * n + 12, carlesonSum (⋃ u ∈ 𝔘₄ k n j l, 𝔗₂ k n j u) f x := by
…
```
Mentions: k, carlesonSum, ℭ₆, 𝔘₄, 𝔗₂
lemma lintegral_carlesonSum_forest For each forest, the integral of the norm of the Carleson sum can be controlled thanks to the forest theorem and to the density control coming from the fact we are away from G₁ line 759 source
Source documentation
For each forest, the integral of the norm of the Carleson sum can be controlled thanks to the forest theorem and to the density control coming from the fact we are away from G₁.

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, Measurable, LE.le, Norm.norm, Set.indicator, OfNat.ofNat and 21 more
Proof uses: TileStructure.Forest, forest, Eq, Finset.sum, Finset.filter, Classical.propDecidable, Finset.univ, TileStructure.Forest.𝔗, MeasurableSpace, Eq.rec, Eq.refl, funext, ENorm, Eq.mpr, Finset, id, congrArg, sum_carlesonSum_of_pairwiseDisjoint, Ne, Function.onFun and 70 more
239 instances, coercions and auxiliary constants left out.

Tactic trace: 38 steps
Open to load the checked before-and-after goal states.
```
lemma lintegral_carlesonSum_forest
    {f : X → ℂ} (hf : Measurable f) (h2f : ∀ x, ‖f x‖ ≤ F.indicator 1 x) :
    ∫⁻ x in G \ G', ‖carlesonSum (⋃ u ∈ 𝔘₄ k n j l, 𝔗₂ k n j u) f x‖ₑ ≤
    C2_0_4 a q n * (2 ^ (2 * a + 5) * volume F / volume G) ^ (q⁻¹ - 2⁻¹) *
    (volume F) ^ (1/2 : ℝ) * (volume G) ^ (1/2 : ℝ) := by
…
```
Mentions: G', carlesonSum, 𝔘₄, k, 𝔗₂
lemma lintegral_carlesonSum_forest' For each forest, the integral of the norm of the Carleson sum can be controlled thanks to the forest theorem and to the density control coming from the fact we are away from G₁ line 803 source
Source documentation
For each forest, the integral of the norm of the Carleson sum can be controlled thanks to the forest theorem and to the density control coming from the fact we are away from G₁. Second version, with the volume of F.

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, Measurable, LE.le, Norm.norm, Set.indicator, OfNat.ofNat and 21 more
Proof uses: LE.le.trans, lintegral_carlesonSum_forest, Eq.mpr, id, Eq, congr, congrArg, Eq.trans, congrFun', mul_assoc, mul_le_mul_right, div_eq_mul_inv, ENNReal.mul_rpow_of_nonneg, inv_q_sub_half_nonneg, one_mul, Trans.trans, rfl, mul_le_mul', ENNReal.rpow_le_rpow_of_exponent_le, one_le_two and 90 more
268 instances, coercions and auxiliary constants left out.

Tactic trace: 34 steps
Open to load the checked before-and-after goal states.
```
lemma lintegral_carlesonSum_forest'
    {f : X → ℂ} (hf : Measurable f) (h2f : ∀ x, ‖f x‖ ≤ F.indicator 1 x) :
    ∫⁻ x in G \ G', ‖carlesonSum (⋃ u ∈ 𝔘₄ k n j l, 𝔗₂ k n j u) f x‖ₑ ≤
    C2_0_4 a q n * 2 ^ (a + 5/2 : ℝ) * (volume G) ^ (1 - q⁻¹) * (volume F) ^ (q⁻¹) := by
…
```
Mentions: G', carlesonSum, 𝔘₄, k, 𝔗₂
lemma forest_union_aux Putting all the above decompositions together, one obtains a control of the integral of the full Carleson sum over 𝔓₁, as a sum over all the forests line 842 source
Source documentation
Putting all the above decompositions together, one obtains a control of the integral of the full Carleson sum over 𝔓₁, as a sum over all the forests.

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, Norm.norm, Set.indicator, OfNat.ofNat, Measurable and 22 more
Proof uses: Trans.trans, Eq, C2_0_4, Set.iUnion, 𝔓, Membership.mem, 𝔘₄, 𝔗₂, ℭ₆, ℭ₅, rfl, Eq.mpr, Sigma, Finset.sigma, Sigma.fst, Sigma.snd, id, congrArg, Eq.trans, Finset.sum_congr and 42 more
195 instances, coercions and auxiliary constants left out.

Tactic trace: 28 steps
Open to load the checked before-and-after goal states.
```
lemma forest_union_aux {f : X → ℂ} (hf : ∀ x, ‖f x‖ ≤ F.indicator 1 x) (h'f : Measurable f) :
    ∫⁻ x in G \ G', ‖carlesonSum 𝔓₁ f x‖ₑ ≤ C2_0_4_base a * 2 ^ (a + 5/2 : ℝ) *
         (volume G) ^ (1 - q⁻¹) * (volume F) ^ (q⁻¹) *
        ∑ n ≤ maxℭ X, ∑ _k ≤ n, ∑ _j ≤ 2 * n + 3, ∑ _l < 4 * n + 12,
          (2 : ℝ≥0∞) ^ (- (q - 1) / q * n : ℝ) := calc
…
```
Mentions: G', carlesonSum, 𝔓₁, maxℭ
lemma forest_union_sum_aux1 line 889 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, LT.lt, OfNat.ofNat, LE.le, Finset.sum, Finset.Iic, HAdd.hAdd, HMul.hMul, Finset.Iio, HPow.hPow, Neg.neg, HDiv.hDiv, HSub.hSub
Proof uses: Eq, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.mpr, id, congrArg, Eq.symm, Eq.refl, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_one, Mathlib.Tactic.Ring.Common.add_pf_add_gt, Mathlib.Tactic.Ring.Common.add_pf_add_zero, Mathlib.Meta.NormNum.instAtLeastTwo, Mathlib.Tactic.Ring.Common.add_mul, Mathlib.Tactic.Ring.Common.mul_add and 194 more
216 instances, coercions and auxiliary constants left out.

Tactic trace: 32 steps
Open to load the checked before-and-after goal states.
lemma forest_union_sum_aux2 line 937 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, LT.lt, OfNat.ofNat, LE.le, ENNReal, Finset.sum, Finset.Iic, HAdd.hAdd, HMul.hMul, Finset.Iio, HPow.hPow, Neg.neg, HDiv.hDiv, HSub.hSub, ENNReal.ofReal
Proof uses: Eq, of_eq_true, Eq.trans, True, congrArg, ENNReal.ofReal_ofNat, eq_self, Eq.mpr, id, congrFun', Finset.sum_congr, Eq.refl, Finset, Membership.mem, ENNReal.ofReal_rpow_of_pos, zero_lt_two, HSMul.hSMul, Finset.card, Finset.sum_const, Nat.card_Iio and 78 more
165 instances, coercions and auxiliary constants left out.

Tactic trace: 30 steps
Open to load the checked before-and-after goal states.
def C5_1_2_optimized An optimized constant for the forest union theorem line 974 source
Source documentation
An optimized constant for the forest union theorem. The constant from the blueprint, defined as C5_1_2 below, is slightly worse.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NNReal
Proof uses: HDiv.hDiv, HMul.hMul, C2_0_4_base, HPow.hPow, Real, OfNat.ofNat, HAdd.hAdd, HSub.hSub
30 instances, coercions and auxiliary constants left out.
```
def C5_1_2_optimized (a : ℕ) (q : ℝ≥0) : ℝ≥0 :=
…
```
lemma forest_union_optimized Version of the forest union result with a better constant line 978 source
Source documentation
Version of the forest union result with a better constant.

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, Norm.norm, Set.indicator, OfNat.ofNat, Measurable and 16 more
Proof uses: LE.le.trans, C2_0_4_base, HAdd.hAdd, HDiv.hDiv, Finset.sum, Finset.Iic, maxℭ, Finset.Iio, Neg.neg, forest_union_aux, Trans.trans, Eq, ENNReal.ofReal, rfl, mul_le_mul', le_refl, HPow, Eq.rec, Eq.refl, Mathlib.Tactic.Ring.of_eq and 70 more
198 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
```
lemma forest_union_optimized {f : X → ℂ} (hf : ∀ x, ‖f x‖ ≤ F.indicator 1 x) (h'f : Measurable f) :
    ∫⁻ x in G \ G', ‖carlesonSum 𝔓₁ f x‖ₑ ≤
    C5_1_2_optimized a nnq * (volume G) ^ (1 - q⁻¹) * (volume F) ^ (q⁻¹) := by
…
```
Mentions: G', carlesonSum, 𝔓₁, C5_1_2_optimized, nnq
lemma C5_1_2_optimized_le' line 1006 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NNReal, LE.le, OfNat.ofNat, C5_1_2_optimized, HDiv.hDiv, HMul.hMul, C2_0_4_base, HPow.hPow, HSub.hSub
Proof uses: Eq, Real, HAdd.hAdd, of_eq_true, Eq.trans, True, congrFun', congrArg, mul_assoc, eq_self, Eq.mpr, id, div_le_div_of_nonneg_right, mul_le_mul', le_refl, Trans.trans, rfl, mul_le_mul, Real.rpow_le_rpow_of_exponent_le, Mathlib.Meta.NormNum.isNat_le_true and 91 more
197 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
def C5_1_2 The constant used in Lemma 5.1.2 line 1030 source
Source documentation
The constant used in Lemma 5.1.2. Has value 2 ^ (441 * a ^ 3) / (q - 1) ^ 4 in the blueprint.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NNReal
Proof uses: HDiv.hDiv, HPow.hPow, OfNat.ofNat, HMul.hMul, HAdd.hAdd, 𝕔, HSub.hSub
24 instances, coercions and auxiliary constants left out.
```
def C5_1_2 (a : ℕ) (q : ℝ≥0) : ℝ≥0 := 2 ^ ((3 * 𝕔 + 16 + 5 * (𝕔 / 4)) * a ^ 3) / (q - 1) ^ 4
…
```
lemma C5_1_2_pos line 1033 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, LT.lt, NNReal, OfNat.ofNat, C5_1_2, nnq
Proof uses: id, div_pos, HPow.hPow, HMul.hMul, HAdd.hAdd, 𝕔, HDiv.hDiv, HSub.hSub, pow_pos, zero_lt_two, Eq.mpr, Eq, one_lt_nnq
65 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma C5_1_2_optimized_le line 1040 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, LE.le, NNReal, C5_1_2_optimized, nnq, C5_1_2
Proof uses: LE.le.trans_eq, HDiv.hDiv, HMul.hMul, C2_0_4_base, HPow.hPow, OfNat.ofNat, HSub.hSub, C5_1_2_optimized_le', KernelProofData.four_le_a, Eq.mpr, Eq, HAdd.hAdd, 𝕔, id, congrFun', congrArg, C2_0_4_base_def, Eq.symm, NNReal.rpow_natCast, pow_add and 53 more
76 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma forest_union Documented declaration: forest_union line 1049 source
Source documentation
Lemma 5.1.2 in the blueprint: the integral of the Carleson sum over the set which can naturally be decomposed as a union of forests can be controlled, thanks to the estimate for a single forest.

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, Norm.norm, Set.indicator, OfNat.ofNat, Measurable and 16 more
Proof uses: LE.le.trans, C5_1_2_optimized, forest_union_optimized, mul_le_mul', C5_1_2_optimized_le, le_refl
105 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma forest_union {f : X → ℂ} (hf : ∀ x, ‖f x‖ ≤ F.indicator 1 x) (h'f : Measurable f) :
    ∫⁻ x in G \ G', ‖carlesonSum 𝔓₁ f x‖ₑ ≤
    C5_1_2 a nnq * (volume G) ^ (1 - q⁻¹) * (volume F) ^ (q⁻¹) := by
…
```
Mentions: G', carlesonSum, 𝔓₁, C5_1_2, nnq