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

50 declarations, 0 contain sorry, 0 declared as axioms

Section 5.5 and Lemma 5.1.3

Imports (5)

Imported by 2 files

def 𝔓pos The set 𝔓_{G\G'} in the blueprint line 24 source
Source documentation
The set 𝔓_{G\G'} in the blueprint

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, LT.lt, ENNReal, OfNat.ofNat, MeasureTheory.Measure, MeasureTheory.MeasureSpace.volume, Inter.inter, 𝓘, Compl.compl, G'
39 instances, coercions and auxiliary constants left out.
```
def 𝔓pos : Set (𝔓 X) := { p : 𝔓 X | 0 < volume (𝓘 p ∩ G ∩ G'ᶜ) }
```
Mentions: 𝔓, 𝓘
lemma exists_mem_aux𝓒 line 26 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, LT.lt, ENNReal, OfNat.ofNat, MeasureTheory.Measure and 6 more
Proof uses: Top.top, volume_coeGrid_lt_top, LE.le, HDiv.hDiv, Eq.mpr, HMul.hMul, id, Eq, congrArg, propext, ENNReal.le_div_iff_mul_le, Or.inl, Ne, LT.lt.ne', Or.inr, LT.lt.ne, one_mul, MeasureTheory.measure_mono, Set.inter_subset_right, Not and 46 more
173 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
lemma exists_k_of_mem_𝔓pos line 47 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, 𝔓pos, Exists, TilesAt
Proof uses: Set.ofPred, Grid, aux𝓒, 𝓘, Set.Nonempty, LT.lt, ENNReal, OfNat.ofNat, MeasureTheory.Measure, MeasureTheory.MeasureSpace.volume, Inter.inter, Eq.mpr, id, Eq, congrArg, Set.inter_comm, LT.lt.trans_le, Compl.compl, G', Eq.mp and 47 more
89 instances, coercions and auxiliary constants left out.

Tactic trace: 26 steps
Open to load the checked before-and-after goal states.
lemma dens'_le_of_mem_𝔓pos line 65 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, 𝔓pos, LE.le, ENNReal and 5 more
Proof uses: id, Eq.mpr, iSup, TilesAt, TileLike, smul, HDiv.hDiv, HMul.hMul, MeasureTheory.Measure, MeasureTheory.MeasureSpace.volume, E₂, 𝓘, Eq, congrFun', congrArg, funext, iSup_congr_Prop, Iff.of_eq, Eq.refl, iSup_iSup_eq_left and 107 more
177 instances, coercions and auxiliary constants left out.

Tactic trace: 26 steps
Open to load the checked before-and-after goal states.
lemma exists_E₂_volume_pos_of_mem_𝔓pos line 84 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, 𝔓pos, Exists, LT.lt and 5 more
Proof uses: MeasureTheory.exists_measure_pos_of_not_measure_iUnion_null, id, Ne, Set.iUnion, Eq.mpr, Inter.inter, 𝓘, Set.preimage, FunctionDistances.Θ, MeasureTheory.SimpleFunc, Metric.ball, WithFunctionDistance, 𝔠, HDiv.hDiv, HPow.hPow, 𝔰, PreTileStructure.𝒬, Eq, congrArg, Eq.symm and 18 more
83 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma dens'_pos_of_mem_𝔓pos line 94 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, 𝔓pos, TilesAt, LT.lt and 4 more
Proof uses: id, Eq.mpr, iSup, LE.le, TileLike, smul, HDiv.hDiv, HMul.hMul, HPow.hPow, Neg.neg, MeasureTheory.Measure, MeasureTheory.MeasureSpace.volume, E₂, 𝓘, Eq, congrArg, funext, iSup_congr_Prop, Iff.of_eq, Eq.refl and 45 more
152 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
lemma exists_k_n_of_mem_𝔓pos line 104 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, 𝔓pos, Exists, And and 2 more
Proof uses: TilesAt, exists_k_of_mem_𝔓pos, Exists.intro, LT.lt, ENNReal, OfNat.ofNat, dens', Singleton.singleton, dens'_pos_of_mem_𝔓pos, HPow.hPow, Neg.neg, dens'_le_of_mem_𝔓pos, Top.top, LE.le.trans_lt, ENNReal.zpow_lt_top, of_eq_true, Not, Eq, Eq.trans, False and 65 more
144 instances, coercions and auxiliary constants left out.

Tactic trace: 29 steps
Open to load the checked before-and-after goal states.
lemma two_mul_n_add_six_lt line 138 source
lemma exists_j_of_mem_𝔓pos_ℭ line 148 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, 𝔓pos, ℭ, LE.le and 8 more
Proof uses: LT.lt, ENNReal, MeasureTheory.Measure, MeasureTheory.MeasureSpace.volume, Inter.inter, Compl.compl, G', 𝓘, LT.lt.trans_le, Eq.mp, congrArg, Eq.symm, Set.inter_assoc, Set.inter_comm, Set.ofPred, propext, Set.mem_ofPred, 𝔓pos.eq_1, MeasureTheory.measure_mono, Set.inter_subset_left and 80 more
144 instances, coercions and auxiliary constants left out.

Tactic trace: 38 steps
Open to load the checked before-and-after goal states.
lemma exists_k_n_j_of_mem_𝔓pos line 181 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, 𝔓pos, Exists, And and 7 more
Proof uses: ℭ, exists_k_n_of_mem_𝔓pos, Exists.intro, And.intro, exists_j_of_mem_𝔓pos_ℭ
42 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
def ℜ₀ The union occurring in the statement of Lemma 5.5.1 containing 𝔏₀ line 187 source
Source documentation
The union occurring in the statement of Lemma 5.5.1 containing 𝔏₀

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, 𝔓pos, Set.iUnion, LE.le, 𝔏₀
28 instances, coercions and auxiliary constants left out.
```
def ℜ₀ : Set (𝔓 X) := 𝔓pos ∩ ⋃ (n : ℕ) (k ≤ n), 𝔏₀ k n
```
Mentions: 𝔓, 𝔓pos, k, 𝔏₀
def ℜ₁ The union occurring in the statement of Lemma 5.5.1 containing 𝔏₁ line 190 source
Source documentation
The union occurring in the statement of Lemma 5.5.1 containing 𝔏₁

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, 𝔓pos, Set.iUnion, LE.le, HAdd.hAdd, HMul.hMul, OfNat.ofNat, defaultZ, 𝔏₁
33 instances, coercions and auxiliary constants left out.
```
def ℜ₁ : Set (𝔓 X) := 𝔓pos ∩ ⋃ (n : ℕ) (k ≤ n) (j ≤ 2 * n + 3) (l ≤ Z * (n + 1)), 𝔏₁ k n j l
```
Mentions: 𝔓, 𝔓pos, k, 𝔏₁
def ℜ₂ The union occurring in the statement of Lemma 5.5.1 containing 𝔏₂ line 193 source
Source documentation
The union occurring in the statement of Lemma 5.5.1 containing 𝔏₂

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, 𝔓pos, Set.iUnion, LE.le, HAdd.hAdd, HMul.hMul, OfNat.ofNat, 𝔏₂
33 instances, coercions and auxiliary constants left out.
```
def ℜ₂ : Set (𝔓 X) := 𝔓pos ∩ ⋃ (n : ℕ) (k ≤ n) (j ≤ 2 * n + 3), 𝔏₂ k n j
```
Mentions: 𝔓, 𝔓pos, k, 𝔏₂
def ℜ₃ The union occurring in the statement of Lemma 5.5.1 containing 𝔏₃ line 196 source
Source documentation
The union occurring in the statement of Lemma 5.5.1 containing 𝔏₃

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, 𝔓pos, Set.iUnion, LE.le, HAdd.hAdd, HMul.hMul, OfNat.ofNat, defaultZ, 𝔏₃
33 instances, coercions and auxiliary constants left out.
```
def ℜ₃ : Set (𝔓 X) := 𝔓pos ∩ ⋃ (n : ℕ) (k ≤ n) (j ≤ 2 * n + 3) (l ≤ Z * (n + 1)), 𝔏₃ k n j l
```
Mentions: 𝔓, 𝔓pos, k, 𝔏₃
lemma mem_iUnion_iff_mem_of_mem_ℭ Lemma allowing to peel ⋃ (n : ℕ) (k ≤ n) from unions in the proof of Lemma 5.5.1 line 199 source
Source documentation
Lemma allowing to peel ⋃ (n : ℕ) (k ≤ n) from unions in the proof of Lemma 5.5.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, 𝔓, And, Membership.mem, ℭ, LE.le and 2 more
Proof uses: Eq.mpr, Exists, id, Eq, congrFun', congrArg, Eq.trans, funext, Iff.intro, Prod, Prod.mk, Set.PairwiseDisjoint.elim, Set.univ, Prod.fst, Prod.snd, pairwiseDisjoint_ℭ, Set.mem_univ, Iff.mpr, Not, Disjoint and 10 more
51 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
lemma mem_iUnion_iff_mem_of_mem_ℭ {f : ℕ → ℕ → Set (𝔓 X)} (hp : p ∈ ℭ k n ∧ k ≤ n)
    (hf : ∀ k n, f k n ⊆ ℭ k n) : p ∈ ⋃ (n : ℕ) (k ≤ n), f k n ↔ p ∈ f k n := by
…
```
Mentions: 𝔓, ℭ, k
lemma mem_iUnion_iff_mem_of_mem_ℭ₁ Lemma allowing to peel ⋃ (j ≤ 2 * n + 3) from unions in the proof of Lemma 5.5.1 line 210 source
Source documentation
Lemma allowing to peel ⋃ (j ≤ 2 * n + 3) from unions in the proof of Lemma 5.5.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, 𝔓, And, Membership.mem, ℭ₁, LE.le and 5 more
Proof uses: Eq.mpr, Exists, id, Eq, congrFun', congrArg, Eq.trans, funext, Iff.intro, Set.PairwiseDisjoint.elim, Set.univ, pairwiseDisjoint_ℭ₁, Set.mem_univ, Iff.mpr, Not, Disjoint, Set.not_disjoint_iff, Exists.intro, And.intro, And.left and 3 more
61 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
lemma mem_iUnion_iff_mem_of_mem_ℭ₁ {f : ℕ → Set (𝔓 X)} (hp : p ∈ ℭ₁ k n j ∧ j ≤ 2 * n + 3)
    (hf : ∀ j, f j ⊆ ℭ₁ k n j) : p ∈ ⋃ (j ≤ 2 * n + 3), f j ↔ p ∈ f j := by
…
```
Mentions: 𝔓, ℭ₁, k
lemma notMem_ℭ₅_iff_mem_𝔏₃ line 219 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, HAdd.hAdd, HMul.hMul, OfNat.ofNat and 10 more
Proof uses: ℭ₃, And.intro, dite, ℭ₄, Classical.propDecidable, id, Set.maxLayer, Eq.mpr, True, Eq, congrArg, eq_true, iff_true, Mathlib.Tactic.Contrapose.contrapose₄, ℭ₅_subset_ℭ₄, Eq.mp, true_implies, implies_congr, Eq.refl, And and 39 more
67 instances, coercions and auxiliary constants left out.

Tactic trace: 23 steps
Open to load the checked before-and-after goal states.
lemma antichain_decomposition Lemma 5.5.1 line 251 source
Source documentation
Lemma 5.5.1.
We will not use the lemma in this form, as to decompose the Carleson sum it is also crucial that the union is disjoint. This is easier to formalize by decomposing into successive terms, taking advantage of disjointess at each step, instead of doing everything in one go. Still, we keep this lemma as it corresponds to the blueprint, and the key steps of its proof will also be the key steps when doing the successive decompositions.

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, 𝔓, Inter.inter, 𝔓pos, Compl.compl and 6 more
Proof uses: id, Set.iUnion, LE.le, 𝔏₀, HAdd.hAdd, HMul.hMul, OfNat.ofNat, defaultZ, 𝔏₁, 𝔏₂, 𝔏₃, Eq.mpr, ℭ₅, congrArg, Eq.trans, congrFun', Set.ext, Iff, Membership.mem, And and 54 more
68 instances, coercions and auxiliary constants left out.

Tactic trace: 69 steps
Open to load the checked before-and-after goal states.
```
lemma antichain_decomposition : 𝔓pos (X := X) ∩ 𝔓₁ᶜ = ℜ₀ ∪ ℜ₁ ∪ ℜ₂ ∪ ℜ₃ := by
…
```
Mentions: 𝔓pos, ℜ₀, ℜ₁, ℜ₂, ℜ₃
def 𝔏₀' The subset 𝔏₀(k, n, l) of 𝔏₀(k, n), given in Lemma 5.5.3 line 291 source
Source documentation
The subset 𝔏₀(k, n, l) of 𝔏₀(k, n), given in Lemma 5.5.3. We use the name 𝔏₀' in Lean.

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.minLayer, 𝔏₀
27 instances, coercions and auxiliary constants left out.
```
def 𝔏₀' (k n l : ℕ) : Set (𝔓 X) := (𝔏₀ k n).minLayer l
```
Mentions: k, 𝔓, 𝔏₀
lemma ceil_log2_le_floor_four_add_log2 Logarithmic inequality used in the proof of Lemma 5.5.2 line 294 source
Source documentation
Logarithmic inequality used in the proof of Lemma 5.5.2.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LE.le, OfNat.ofNat, Nat, Nat.ceil, Real.logb, HDiv.hDiv, HAdd.hAdd, Inv.inv, Nat.floor
Proof uses: Trans.trans, GE.ge, HPow.hPow, add_le_add, Real.logb_le_logb_of_le, one_lt_two, Real.rpow_pos_of_pos, Mathlib.Meta.Positivity.pos_of_isNat, inferInstance, PartialOrder, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Bool, Nat.ble, le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HMul.hMul and 127 more
156 instances, coercions and auxiliary constants left out.

Tactic trace: 28 steps
Open to load the checked before-and-after goal states.
```
lemma ceil_log2_le_floor_four_add_log2 {l : ℝ} (hl : 2 ≤ l) :
    ⌈Real.logb 2 ((l + 6 / 5) / 5⁻¹)⌉₊ ≤ ⌊4 + Real.logb 2 l⌋₊ := by
…
```
def 𝔒 The set 𝔒 in the proof of Lemma 5.5.2 line 321 source
Source documentation
The set 𝔒 in the proof of Lemma 5.5.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, 𝔓, Finset
Proof uses: Finset.filter, And, Eq, Grid, 𝓘, Not, Disjoint, WithFunctionDistance, 𝔠, HDiv.hDiv, HPow.hPow, 𝔰, OfNat.ofNat, Metric.ball, PreTileStructure.𝒬, TileStructure.Ω, Classical.propDecidable, Finset.univ
50 instances, coercions and auxiliary constants left out.
```
def 𝔒 (p' : 𝔓 X) (l : ℝ≥0) : Finset (𝔓 X) :=
…
```
Mentions: 𝔓
lemma card_𝔒 line 325 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, OfNat.ofNat, Finset.card, 𝔒 and 3 more
Proof uses: Set.PairwiseDisjoint, WithFunctionDistance, 𝔠, HDiv.hDiv, 𝔰, Finset, Metric.ball, PreTileStructure.𝒬, Inv.inv, Membership.mem, Ne, id, Function.onFun, Disjoint, Eq.mpr, c, 𝓘, s, Eq, Eq.rec and 108 more
201 instances, coercions and auxiliary constants left out.

Tactic trace: 45 steps
Open to load the checked before-and-after goal states.
lemma lt_quotient_rearrange line 382 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, 𝔓, LT.lt, ENNReal, HPow.hPow, OfNat.ofNat and 8 more
Proof uses: Eq.mpr, eq_of_heq, LT, Eq, HEq, Eq.refl, HEq.refl, Eq.symm, Inv.inv, id, congrArg, ENNReal.div_eq_inv_mul, ENNReal.zpow_neg, neg_neg, ENNReal.coe_mul, mul_rotate, mul_assoc, ENNReal.coe_pow, zpow_natCast, HMul and 10 more
130 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma l_upper_bound line 393 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, OfNat.ofNat, LT.lt, ENNReal and 9 more
Proof uses: ENNReal.div_le_of_le_mul, Eq.mpr, id, Eq, congrArg, one_mul, MeasureTheory.measure_mono, E₂_subset, LT.lt.trans_le, lt_quotient_rearrange, Trans.trans, le_self_pow₀, LE.le.trans, one_le_two, Not.intro, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HAdd.hAdd, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr and 78 more
206 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
lemma exists_𝔒_with_le_quotient line 408 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, OfNat.ofNat, LT.lt, ENNReal and 15 more
Proof uses: Finset.card, Nat.floor, card_𝔒, Finset.sum, Trans.trans, Eq, Set.iUnion, lt_quotient_rearrange, ENNReal.div_le_div, MeasureTheory.measure_mono, Eq.mpr, TileLike.toSet, toTileLike, id, congrArg, funext, Set.iUnion_congr_Prop, Iff.of_eq, Eq.refl, smul and 83 more
188 instances, coercions and auxiliary constants left out.

Tactic trace: 33 steps
Open to load the checked before-and-after goal states.
lemma iUnion_L0' Main part of Lemma 5.5.2 line 449 source
Source documentation
Main part of Lemma 5.5.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, LT.lt, 𝔏₀' and 1 more
Proof uses: Iff.mpr, Set.minLayer, LTSeries, Membership.mem, RelSeries.length, Set.ofPred, Prod, FiniteDimensionalOrder.match_1, Set.iUnion_lt_minLayer_iff_bounded_series, Not, Exists, id, False, RelSeries.last, ENNReal, HPow.hPow, OfNat.ofNat, HSub.hSub, HMul.hMul, dens' and 192 more
241 instances, coercions and auxiliary constants left out.

Tactic trace: 90 steps
Open to load the checked before-and-after goal states.
```
lemma iUnion_L0' : ⋃ (l < n), 𝔏₀' (X := X) k n l = 𝔏₀ k n := by
…
```
Mentions: 𝔏₀', k, 𝔏₀
lemma pairwiseDisjoint_L0' Part of Lemma 5.5.2 line 524 source
Source documentation
Part of Lemma 5.5.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, 𝔓, Set.univ, 𝔏₀'
Proof uses: Set.pairwiseDisjoint_minLayer, 𝔏₀
36 instances, coercions and auxiliary constants left out.
```
lemma pairwiseDisjoint_L0' : univ.PairwiseDisjoint (𝔏₀' (X := X) k n) := pairwiseDisjoint_minLayer
```
Mentions: 𝔏₀', k
lemma antichain_L0' Part of Lemma 5.5.2 line 527 source
Source documentation
Part of Lemma 5.5.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, IsAntichain, 𝔓, LE.le, 𝔏₀'
Proof uses: Set.isAntichain_minLayer, 𝔏₀
30 instances, coercions and auxiliary constants left out.
```
lemma antichain_L0' : IsAntichain (· ≤ ·) (𝔏₀' (X := X) k n l) := isAntichain_minLayer
…
```
Mentions: 𝔏₀', k
def ℭ₁' Type synonym of ℭ₁ to apply the Preorder of the proof of Lemma 5.5.3 on line 532 source
Source documentation
Type synonym of ℭ₁ to apply the Preorder of the proof of Lemma 5.5.3 on.
```
private def ℭ₁' (k n j : ℕ) : Type _ := ℭ₁ (X := X) k n j
…
```
Mentions: k, ℭ₁
instance (instance at line 535) line 535 source
instance (instance at line 537) line 537 source
lemma antichain_L2 Lemma 5.5.3 line 546 source
Source documentation
Lemma 5.5.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, IsAntichain, 𝔓, LE.le, 𝔏₂
Proof uses: Decidable.byContradiction, Classical.propDecidable, Not, And, Membership.mem, Exists, LT.lt, False, Eq.mp, Eq.trans, Mathlib.Tactic.Push.not_forall_eq, congrArg, funext, propext, isAntichain_iff_forall_not_lt, TileLike, smul, OfNat.ofNat, Trans.trans, HAdd.hAdd and 131 more
180 instances, coercions and auxiliary constants left out.

Tactic trace: 67 steps
Open to load the checked before-and-after goal states.
```
lemma antichain_L2 : IsAntichain (· ≤ ·) (𝔏₂ (X := X) k n j) := by
…
```
Mentions: 𝔏₂, k
lemma antichain_L1 Part of Lemma 5.5.4 line 598 source
Source documentation
Part of Lemma 5.5.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, IsAntichain, 𝔓, LE.le, 𝔏₁
Proof uses: Set.isAntichain_minLayer, ℭ₁
30 instances, coercions and auxiliary constants left out.
```
lemma antichain_L1 : IsAntichain (· ≤ ·) (𝔏₁ (X := X) k n j l) := isAntichain_minLayer
```
Mentions: 𝔏₁, k
lemma antichain_L3 Part of Lemma 5.5.4 line 601 source
Source documentation
Part of Lemma 5.5.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, IsAntichain, 𝔓, LE.le, 𝔏₃
Proof uses: Set.isAntichain_maxLayer, ℭ₃
30 instances, coercions and auxiliary constants left out.
```
lemma antichain_L3 : IsAntichain (· ≤ ·) (𝔏₃ (X := X) k n j l) := isAntichain_maxLayer
```
Mentions: 𝔏₃, k
lemma carlesonSum_𝔓₁_compl_eq_𝔓pos_inter The Carleson sum over 𝔓₁ᶜ and 𝔓pos ∩ 𝔓₁ᶜ coincide at ae every point of G \ G' line 610 source
Source documentation
The Carleson sum over 𝔓₁ᶜ and 𝔓pos ∩ 𝔓₁ᶜ coincide at ae every point of 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, Filter.Eventually, Membership.mem, SDiff.sdiff, G', Eq and 9 more
Proof uses: Not, Grid, 𝓘, Filter.mp_mem, Set.ofPred, Iff.mp, ENNReal, OfNat.ofNat, MeasureTheory.measure_eq_zero_iff_ae_notMem, Eq.mp, Eq.trans, LT.lt, LE.le, Filter.univ_mem', id, And.intro, And.left, And.right, congrArg, Eq.symm and 38 more
103 instances, coercions and auxiliary constants left out.

Tactic trace: 22 steps
Open to load the checked before-and-after goal states.
```
lemma carlesonSum_𝔓₁_compl_eq_𝔓pos_inter (f : X → ℂ) :
    ∀ᵐ x, x ∈ G \ G' → carlesonSum 𝔓₁ᶜ f x = carlesonSum (𝔓pos (X := X) ∩ 𝔓₁ᶜ) f x := by
…
```
Mentions: G', carlesonSum, 𝔓pos
lemma carlesonSum_𝔓pos_eq_sum The Carleson sum over 𝔓pos ∩ 𝔓₁ᶜ can be decomposed as a sum over the intersections of this set with various ℭ k n line 633 source
Source documentation
The Carleson sum over 𝔓pos ∩ 𝔓₁ᶜ can be decomposed as a sum over the intersections of this set with various ℭ k n.

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, Inter.inter, 𝔓, 𝔓pos and 6 more
Proof uses: Eq.mpr, Sigma, Finset.sigma, Sigma.snd, Sigma.fst, id, congrArg, Finset.sum_sigma', Set.iUnion, Membership.mem, Finset, sum_carlesonSum_of_pairwiseDisjoint, Ne, Function.onFun, Disjoint, Sigma.mk, Prod, Prod.fst, Prod.snd, Prod.mk and 34 more
79 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
```
lemma carlesonSum_𝔓pos_eq_sum {f : X → ℂ} {x : X} :
    carlesonSum (𝔓pos (X := X) ∩ 𝔓₁ᶜ) f x =
…
```
Mentions: carlesonSum, 𝔓pos
lemma carlesonSum_𝔓pos_inter_ℭ_eq_add_sum In each set ℭ k n, the Carleson sum can be decomposed as a sum over 𝔏₀ k n and over various ℭ₁ k n j line 655 source
Source documentation
In each set ℭ k n, the Carleson sum can be decomposed as a sum over 𝔏₀ k n and over various ℭ₁ 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, carlesonSum, Inter.inter, 𝔓 and 11 more
Proof uses: Eq.mpr, id, Eq.rec, Eq.refl, Eq.trans, congrArg, Eq.symm, carlesonSum_inter_add_inter_compl, Set.iUnion, Membership.mem, Finset, sum_carlesonSum_of_pairwiseDisjoint, Set.PairwiseDisjoint.subset, Set.univ, Set.PairwiseDisjoint.mono, pairwiseDisjoint_ℭ₁, Set.inter_subset_right, Set.subset_univ, HAdd, PseudoMetricSpace and 34 more
86 instances, coercions and auxiliary constants left out.

Tactic trace: 28 steps
Open to load the checked before-and-after goal states.
```
lemma carlesonSum_𝔓pos_inter_ℭ_eq_add_sum {f : X → ℂ} {x : X} (hkn : k ≤ n) :
    carlesonSum (𝔓pos ∩ 𝔓₁ᶜ ∩ ℭ k n) f x =
      carlesonSum (𝔓pos ∩ 𝔓₁ᶜ ∩ 𝔏₀ k n) f x
      + ∑ j ≤ 2 * n + 3, carlesonSum (𝔓pos ∩ 𝔓₁ᶜ ∩ ℭ₁ k n j) f x := by
…
```
Mentions: k, carlesonSum, 𝔓pos, ℭ, 𝔏₀, ℭ₁
lemma carlesonSum_𝔓pos_inter_𝔏₀_eq_sum line 682 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, Eq, carlesonSum, Inter.inter, 𝔓, 𝔓pos and 6 more
Proof uses: Eq.mpr, Set.iUnion, Membership.mem, Finset, id, congrArg, sum_carlesonSum_of_pairwiseDisjoint, Set.PairwiseDisjoint.subset, Set.univ, Set.PairwiseDisjoint.mono, pairwiseDisjoint_L0', Set.inter_subset_right, Set.subset_univ, PseudoMetricSpace, Eq.rec, Eq.refl, LT.lt, Eq.symm, iUnion_L0', Set.ext and 14 more
60 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
lemma carlesonSum_𝔓pos_inter_ℭ₁_eq_add_sum In each set ℭ₁ k n j, the Carleson sum can be decomposed as a sum over ℭ₂ k n j and over various 𝔏₁ k n j l line 698 source
Source documentation
In each set ℭ₁ k n j, the Carleson sum can be decomposed as a sum over ℭ₂ k n j and over various 𝔏₁ 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, Eq, carlesonSum, Inter.inter, 𝔓, 𝔓pos and 11 more
Proof uses: Eq.mpr, id, Eq.rec, Eq.refl, Eq.trans, congrArg, Eq.symm, carlesonSum_inter_add_inter_compl, Set.iUnion, Membership.mem, Finset, sum_carlesonSum_of_pairwiseDisjoint, Set.PairwiseDisjoint.subset, Set.univ, Set.PairwiseDisjoint, Set.pairwiseDisjoint_minLayer, Set.PairwiseDisjoint.mono, Set.inter_subset_right, Set.subset_univ, HAdd and 33 more
87 instances, coercions and auxiliary constants left out.

Tactic trace: 27 steps
Open to load the checked before-and-after goal states.
```
lemma carlesonSum_𝔓pos_inter_ℭ₁_eq_add_sum {f : X → ℂ} {x : X} :
    carlesonSum (𝔓pos ∩ 𝔓₁ᶜ ∩ ℭ₁ k n j) f x =
      carlesonSum (𝔓pos ∩ 𝔓₁ᶜ ∩ ℭ₂ k n j) f x
      + ∑ l ≤ Z * (n + 1), carlesonSum (𝔓pos ∩ 𝔓₁ᶜ ∩ 𝔏₁ k n j l) f x := by
…
```
Mentions: carlesonSum, 𝔓pos, ℭ₁, k, ℭ₂, 𝔏₁
lemma carlesonSum_𝔓pos_inter_ℭ₂_eq_add_sum In each set ℭ₂ k n j, the Carleson sum can be decomposed as a sum over 𝔏₂ k n j and over various 𝔏₃ k n j l line 727 source
Source documentation
In each set ℭ₂ k n j, the Carleson sum can be decomposed as a sum over 𝔏₂ k n j and over various 𝔏₃ 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, HAdd.hAdd, HMul.hMul, OfNat.ofNat, Eq and 12 more
Proof uses: Eq.mpr, id, Eq.rec, Eq.refl, Eq.trans, congrArg, Eq.symm, carlesonSum_inter_add_inter_compl, Set.iUnion, Membership.mem, Finset, sum_carlesonSum_of_pairwiseDisjoint, Set.PairwiseDisjoint.subset, Set.univ, Set.PairwiseDisjoint, Set.pairwiseDisjoint_minLayer, OrderDual, ℭ₃, Set.PairwiseDisjoint.mono, Set.inter_subset_right and 38 more
97 instances, coercions and auxiliary constants left out.

Tactic trace: 28 steps
Open to load the checked before-and-after goal states.
```
lemma carlesonSum_𝔓pos_inter_ℭ₂_eq_add_sum {f : X → ℂ} {x : X} (hkn : k ≤ n) (hj : j ≤ 2 * n + 3) :
    carlesonSum (𝔓pos ∩ 𝔓₁ᶜ ∩ ℭ₂ k n j) f x =
      carlesonSum (𝔓pos ∩ 𝔓₁ᶜ ∩ 𝔏₂ k n j) f x
      + ∑ l ≤ Z * (n + 1), carlesonSum (𝔓pos ∩ 𝔓₁ᶜ ∩ 𝔏₃ k n j l) f x := by
…
```
Mentions: k, carlesonSum, 𝔓pos, ℭ₂, 𝔏₂, 𝔏₃
lemma lintegral_carlesonSum_𝔓₁_compl_le_sum_lintegral Documented declaration: lintegral_carlesonSum_𝔓₁_compl_le_sum_lintegral line 762 source
Source documentation
Putting together all the previous decomposition lemmas, one gets an estimate of the integral of ‖carlesonSum 𝔓₁ᶜ f x‖ₑ by a sum of integrals of the same form over various subsets of 𝔓, which are all antichains by design.

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, ENNReal, MeasureTheory.lintegral, MeasureTheory.Measure.restrict and 22 more
Proof uses: Trans.trans, Eq, ℭ₂, ℭ₁, 𝔏₀, ℭ, rfl, MeasureTheory.lintegral_congr_ae, Iff.mpr, Filter.Eventually, MeasureTheory.ae, MeasureTheory.Measure, Membership.mem, MeasureTheory.ae_restrict_iff', MeasurableSet.diff, ProofData.measurableSet_G, measurable_G', Filter.mp_mem, Set.ofPred, carlesonSum_𝔓₁_compl_eq_𝔓pos_inter and 40 more
130 instances, coercions and auxiliary constants left out.

Tactic trace: 69 steps
Open to load the checked before-and-after goal states.
```
lemma lintegral_carlesonSum_𝔓₁_compl_le_sum_lintegral {f : X → ℂ} (h'f : Measurable f) :
    ∫⁻ x in G \ G', ‖carlesonSum 𝔓₁ᶜ f x‖ₑ ≤
        (∑ n ≤ maxℭ X, ∑ k ≤ n, ∑ l < n,
          ∫⁻ x in G \ G', ‖carlesonSum (𝔓pos ∩ 𝔓₁ᶜ ∩ 𝔏₀' k n l) f x‖ₑ)
      + (∑ n ≤ maxℭ X, ∑ k ≤ n, ∑ j ≤ 2 * n + 3, ∑ l ≤ Z * (n + 1),
          ∫⁻ x in G \ G', ‖carlesonSum (𝔓pos ∩ 𝔓₁ᶜ ∩ 𝔏₁ k n j l) f x‖ₑ)
      + (∑ n ≤ maxℭ X, ∑ k ≤ n, ∑ j ≤ 2 * n + 3,
          ∫⁻ x in G \ G', ‖carlesonSum (𝔓pos ∩ 𝔓₁ᶜ ∩ 𝔏₂ k n j) f x‖ₑ)
      + (∑ n ≤ maxℭ X, ∑ k ≤ n, ∑ j ≤ 2 * n + 3, ∑ l ≤ Z * (n + 1),
          ∫⁻ x in G \ G', ‖carlesonSum (𝔓pos ∩ 𝔓₁ᶜ ∩ 𝔏₃ k n j l) f x‖ₑ) := calc
…
```
Mentions: G', carlesonSum, maxℭ, k, 𝔓pos, 𝔏₀', 𝔏₁, 𝔏₂, 𝔏₃
lemma lintegral_enorm_carlesonSum_le_of_isAntichain_subset_ℭ Custom version of the antichain operator theorem, in the specific form we need to handle the various terms in the previous statement line 861 source
Source documentation
Custom version of the antichain operator theorem, in the specific form we need to handle the various terms in the previous statement.

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 and 25 more
Proof uses: le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Int.rawCast, inferInstance, Ring, Int.negOfNat, Nat.rawCast, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.mpr, Eq, id, Eq.symm, Eq.refl and 250 more
343 instances, coercions and auxiliary constants left out.

Tactic trace: 77 steps
Open to load the checked before-and-after goal states.
```
lemma lintegral_enorm_carlesonSum_le_of_isAntichain_subset_ℭ
    {f : X → ℂ} {𝔄 : Set (𝔓 X)} (hf : ∀ x, ‖f x‖ ≤ F.indicator 1 x) (h'f : Measurable f)
    (hA : IsAntichain (· ≤ ·) 𝔄) (h'A : 𝔄 ⊆ ℭ k n) :
    ∫⁻ x in G \ G', ‖carlesonSum (𝔓pos ∩ 𝔓₁ᶜ ∩ 𝔄) f x‖ₑ
    ≤ C2_0_3 a nnq * 2 ^ (a + 3) * volume G ^ (1 - q⁻¹) * volume F ^ (q⁻¹)
      * 2 ^ (- ((q - 1) / (8 * a ^ 4) * n)) := by
…
```
Mentions: 𝔓, ℭ, k, G', carlesonSum, 𝔓pos, C2_0_3, nnq
lemma lintegral_carlesonSum_𝔓₁_compl_le_sum_aux1 line 952 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, LE.le, Finset.sum, Finset.Iic, HMul.hMul, HAdd.hAdd, OfNat.ofNat, defaultZ, HPow.hPow, Neg.neg, HDiv.hDiv, HSub.hSub
Proof uses: Eq.mpr, id, Eq, congrFun', congrArg, Eq.trans, Finset.sum_congr, Eq.refl, Finset, Membership.mem, add_mul, Finset.sum_add_distrib, congr, mul_assoc, LT.lt, lt_of_not_ge, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr and 229 more
246 instances, coercions and auxiliary constants left out.

Tactic trace: 50 steps
Open to load the checked before-and-after goal states.
lemma lintegral_carlesonSum_𝔓₁_compl_le_sum_aux2 line 1039 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, LE.le, ENNReal, Finset.sum, Finset.Iic, HMul.hMul, HAdd.hAdd, OfNat.ofNat, defaultZ, HPow.hPow, Neg.neg, HDiv.hDiv, HSub.hSub, nnq
Proof uses: LT.lt, lt_of_not_ge, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Int.rawCast, inferInstance, Ring, Int.negOfNat, Nat.rawCast, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.mpr, Eq, id, Eq.symm, Eq.refl and 76 more
166 instances, coercions and auxiliary constants left out.

Tactic trace: 26 steps
Open to load the checked before-and-after goal states.
def C5_1_3_optimized An optimized constant for Lemma 5.1.3 line 1076 source
Source documentation
An optimized constant for Lemma 5.1.3.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NNReal
Proof uses: HDiv.hDiv, HMul.hMul, C2_0_3, HPow.hPow, OfNat.ofNat, HAdd.hAdd, HSub.hSub
24 instances, coercions and auxiliary constants left out.
```
def C5_1_3_optimized (a : ℕ) (q : ℝ≥0) := C2_0_3 a q * 2 ^ (29 * a + 23) / (q - 1) ^ 4
```
Mentions: C2_0_3
def C5_1_3 The constant used in Lemma 5.1.3 line 1080 source
Source documentation
The constant used in Lemma 5.1.3. Has value 2 ^ (120 * a ^ 3) / (q - 1) ^ 5 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_3 (a : ℕ) (q : ℝ≥0) : ℝ≥0 := 2 ^ ((𝕔 + 8 + 𝕔 / 8) * a ^ 3) / (q - 1) ^ 5
…
```
lemma C5_1_3_pos line 1083 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_3, nnq
Proof uses: HSub.hSub, tsub_pos_of_lt, one_lt_nnq, id, div_pos, HPow.hPow, HMul.hMul, HAdd.hAdd, 𝕔, HDiv.hDiv, pow_pos, Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Bool, Nat.ble
56 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma C5_1_3_optimized_le_C5_1_3 line 1089 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_3_optimized, nnq, C5_1_3
Proof uses: id, Trans.trans, Eq, HDiv.hDiv, HMul.hMul, HPow.hPow, OfNat.ofNat, HAdd.hAdd, 𝕔, HSub.hSub, KernelProofData.four_le_a, div_le_div_of_nonneg_right, mul_le_mul', le_refl, pow_le_pow_right₀, one_le_two, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.cast_pos and 54 more
95 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
lemma forest_complement_optimized line 1105 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, Norm.norm, Set.indicator, OfNat.ofNat, Measurable and 18 more
Proof uses: Trans.trans, Eq, HDiv.hDiv, C2_0_3, HAdd.hAdd, Finset.sum, Finset.Iic, maxℭ, defaultZ, Neg.neg, Finset.Iio, Inter.inter, 𝔓pos, 𝔏₀', 𝔏₁, 𝔏₂, 𝔏₃, rfl, lintegral_carlesonSum_𝔓₁_compl_le_sum_lintegral, add_le_add and 94 more
196 instances, coercions and auxiliary constants left out.

Tactic trace: 34 steps
Open to load the checked before-and-after goal states.
lemma forest_complement Lemma 5.1.3, proving the bound on the integral of the Carleson sum over all leftover tiles which do not fit in a forest line 1178 source
Source documentation
Lemma 5.1.3, proving the bound on the integral of the Carleson sum over all leftover tiles which do not fit in a forest. It follows from a careful grouping of these tiles into finitely many antichains.

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 18 more
Proof uses: LE.le.trans, C5_1_3_optimized, forest_complement_optimized, mul_le_mul', C5_1_3_optimized_le_C5_1_3, le_refl
109 instances, coercions and auxiliary constants left out.

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