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

56 declarations, 0 contain sorry, 0 declared as axioms

Lemma 7.4.4

Imports (5)

Imported by 2 files

lemma TileStructure.Forest.estimate_C7_4_5 line 27 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, NNReal, TileStructure.Forest.C7_4_5, HMul.hMul, HPow.hPow, HAdd.hAdd, 𝕔, HDiv.hDiv, Real, Neg.neg
Proof uses: Eq.mpr, defaultZ, id, Eq, congrFun', congrArg, TileStructure.Forest.C7_4_5_def, neg_div, Inv.inv, congr, NNReal.rpow_neg, div_le_div₀, le_of_lt, pow_pos, Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Bool, Nat.ble and 103 more
221 instances, coercions and auxiliary constants left out.

Tactic trace: 23 steps
Open to load the checked before-and-after goal states.
lemma TileStructure.Forest.estimate_C7_4_6 line 43 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, NNReal, TileStructure.Forest.C7_4_6, HMul.hMul, HPow.hPow, HAdd.hAdd, 𝕔, HDiv.hDiv, Real, Neg.neg
Proof uses: Eq.mpr, TileStructure.Forest.C7_2_1, TileStructure.Forest.C7_6_2, id, Eq, congrFun', congrArg, TileStructure.Forest.C7_4_6_def, TileStructure.Forest.C7_2_1_def, C2_1_3, defaultZ, defaultκ, TileStructure.Forest.C7_6_2_def, Eq.trans, Inv.inv, congr, NNReal.rpow_neg, div_le_div₀, le_of_lt, pow_pos and 133 more
235 instances, coercions and auxiliary constants left out.

Tactic trace: 42 steps
Open to load the checked before-and-after goal states.
lemma TileStructure.Forest.le_C7_4_4 line 81 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, NNReal, HAdd.hAdd, TileStructure.Forest.C7_4_5, TileStructure.Forest.C7_4_6, TileStructure.Forest.C7_4_4
Proof uses: LE.le.trans, HMul.hMul, HPow.hPow, 𝕔, HDiv.hDiv, Real, Neg.neg, add_le_add, TileStructure.Forest.estimate_C7_4_5, TileStructure.Forest.estimate_C7_4_6, Eq.mpr, id, Eq, congr, congrArg, TileStructure.Forest.C7_4_4_def, mul_le_mul', LE.le.trans_eq, add_le_pow_two_add_cube, le_rfl and 44 more
68 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma TileStructure.Forest.correlation_separated_trees_of_subset line 89 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, Ne, LE.le and 18 more
Proof uses: Trans.trans, HAdd.hAdd, TileStructure.Forest.C7_4_5, TileStructure.Forest.C7_4_6, TileStructure.Forest.𝔖₀, SDiff.sdiff, Eq, eq_of_heq, ENorm, HEq, Eq.refl, HEq.refl, Eq.symm, NormedAddCommGroup, NormedSpace, MeasurableSpace, MeasureTheory.Measure, funext, Eq.mpr, id and 35 more
182 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
lemma TileStructure.Forest.cst_disjoint line 123 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, 𝔓, Disjoint, 𝓘, Membership.mem and 7 more
Proof uses: Eq.mpr, Set.indicator, id, congrArg, TileStructure.Forest.adjoint_tile_support2_sum, Function.comp, Eq.symm, Function.comp_apply, Set.indicator_comp_of_zero, of_eq_true, Eq.trans, True, congrFun', map_zero, eq_self, Inter.inter, Set.inter_indicator_mul, EmptyCollection.emptyCollection, Eq.mp, propext and 3 more
86 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma TileStructure.Forest.correlation_separated_trees Lemma 7.4.4 line 131 source
Source documentation
Lemma 7.4.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, 𝔓, Membership.mem, Ne, MeasureTheory.BoundedCompactSupport and 17 more
Proof uses: dite, Disjoint, Classical.propDecidable, of_eq_true, HPow.hPow, 𝕔, Eq.trans, True, congrFun', congrArg, funext, TileStructure.Forest.cst_disjoint, MeasureTheory.integral_zero, enorm_zero, Not, Grid, Or, Classical.em, TileStructure.Forest.correlation_separated_trees_of_subset, Or.resolve_right and 45 more
180 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
```
lemma correlation_separated_trees (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (hu : u₁ ≠ u₂)
    (hg₁ : BoundedCompactSupport g₁) (hg₂ : BoundedCompactSupport g₂) :
    ‖∫ x, adjointCarlesonSum (t u₁) g₁ x * conj (adjointCarlesonSum (t u₂) g₂ x)‖ₑ ≤
    C7_4_4 a n *
    eLpNorm ((𝓘 u₁ ∩ 𝓘 u₂ : Set X).indicator (adjointBoundaryOperator t u₁ g₁) ·) 2 volume *
    eLpNorm ((𝓘 u₁ ∩ 𝓘 u₂ : Set X).indicator (adjointBoundaryOperator t u₂ g₂) ·) 2 volume := by
…
```
Mentions: adjointCarlesonSum, 𝓘, TileStructure.Forest.adjointBoundaryOperator
def TileStructure.Forest.rowDecomp_zornset line 152 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, 𝔓
Proof uses: Inter.inter, Set.ofPred, LE.le, Set.PairwiseDisjoint, 𝓘, Maximal, Grid, Membership.mem, Set.image
43 instances, coercions and auxiliary constants left out.
lemma TileStructure.Forest.mem_rowDecomp_zornset_iff line 156 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, 𝔓, Iff, Membership.mem, TileStructure.Forest.rowDecomp_zornset, And and 6 more
Proof uses: id, Eq.mpr, Inter.inter, Set.ofPred, Eq, congrFun', congrArg, Eq.trans, congr, Set.subset_def, of_eq_true, True, forall_congr, implies_congr, Eq.refl, iff_self
62 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma TileStructure.Forest.rowDecomp_zornset_chain_Union_bound line 163 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, TileStructure.Forest.rowDecomp_zornset, IsChain, And and 2 more
Proof uses: id, Set.ofPred, Set.PairwiseDisjoint, 𝓘, Maximal, Grid, Set.image, Inter.inter, Eq.mp, Eq.trans, congrFun', congrArg, Eq.mpr, Eq, congr, And.intro, Iff.mpr, Set.iUnion₂_subset_iff, IsChain.pairwiseDisjoint_iUnion₂, Set.subset_iUnion₂_of_subset and 1 more
50 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
def TileStructure.Forest.rowDecomp_𝔘 line 175 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, 𝔓
Proof uses: WellFounded.Nat.fix, InvImage, LT.lt, Exists.choose, Maximal, Membership.mem, TileStructure.Forest.rowDecomp_zornset, SDiff.sdiff, TileStructure.Forest.𝔘, Set.iUnion
32 instances, coercions and auxiliary constants left out.
lemma TileStructure.Forest.rowDecomp_𝔘_def line 179 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, Maximal, 𝔓, Membership.mem, TileStructure.Forest.rowDecomp_zornset and 5 more
Proof uses: Eq.mpr, Exists.choose, id, Eq, congrArg, TileStructure.Forest.rowDecomp_𝔘.eq_1, Exists.choose_spec
35 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma TileStructure.Forest.rowDecomp_𝔘_mem_zornset line 184 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, 𝔓, TileStructure.Forest.rowDecomp_zornset, SDiff.sdiff and 4 more
Proof uses: Maximal.prop, TileStructure.Forest.rowDecomp_𝔘_def
33 instances, coercions and auxiliary constants left out.
lemma TileStructure.Forest.rowDecomp_𝔘_subset line 188 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, LE.le, 𝔓, TileStructure.Forest.rowDecomp_𝔘, SDiff.sdiff and 3 more
Proof uses: Membership.mem, TileStructure.Forest.rowDecomp_zornset, TileStructure.Forest.rowDecomp_𝔘_mem_zornset, And.left, And, Set.PairwiseDisjoint, 𝓘, Maximal, Grid, Set.image, Eq.mp, congrArg, propext, TileStructure.Forest.mem_rowDecomp_zornset_iff
47 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma TileStructure.Forest.rowDecomp_𝔘_pairwiseDisjoint line 194 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, Set.PairwiseDisjoint, 𝔓, TileStructure.Forest.rowDecomp_𝔘, 𝓘
Proof uses: Membership.mem, TileStructure.Forest.rowDecomp_zornset, SDiff.sdiff, TileStructure.Forest.𝔘, Set.iUnion, LT.lt, TileStructure.Forest.rowDecomp_𝔘_mem_zornset, And.left, Maximal, Grid, Set.image, And.right, LE.le, And, Eq.mp, congrArg, propext, TileStructure.Forest.mem_rowDecomp_zornset_iff
55 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma TileStructure.Forest.mem_rowDecomp_𝔘_maximal line 200 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, TileStructure.Forest.rowDecomp_𝔘, Maximal and 7 more
Proof uses: TileStructure.Forest.rowDecomp_zornset, TileStructure.Forest.rowDecomp_𝔘_mem_zornset, And.right, Set.PairwiseDisjoint, LE.le, And, Eq.mp, congrArg, propext, TileStructure.Forest.mem_rowDecomp_zornset_iff
51 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma TileStructure.Forest.rowDecomp_𝔘_subset_forest line 206 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, LE.le, 𝔓, TileStructure.Forest.rowDecomp_𝔘, TileStructure.Forest.𝔘
Proof uses: subset_trans, SDiff.sdiff, Set.iUnion, LT.lt, TileStructure.Forest.rowDecomp_𝔘_subset, Set.sdiff_subset
36 instances, coercions and auxiliary constants left out.
def TileStructure.Forest.rowDecomp The row-decomposition of a tree, defined in the proof of Lemma 7.7.1 line 211 source
Source documentation
The row-decomposition of a tree, defined in the proof of Lemma 7.7.1. The indexing is off-by-one compared to 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, TileStructure.Forest, TileStructure.Row
Proof uses: TileStructure.Row.mk, TileStructure.Forest.mk, TileStructure.Forest.rowDecomp_𝔘, 𝔓, TileStructure.Forest.𝔗, TileStructure.Forest.rowDecomp_𝔘_pairwiseDisjoint
33 instances, coercions and auxiliary constants left out.
```
def rowDecomp (t : Forest X n) (j : ℕ) : Row X n where
…
```
Mentions: TileStructure.Forest, TileStructure.Row
lemma TileStructure.Forest.mem_forest_of_mem line 224 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, TileStructure.Row, TileStructure.Forest.rowDecomp
Proof uses: TileStructure.Forest.rowDecomp_𝔘_subset_forest
29 instances, coercions and auxiliary constants left out.
lemma TileStructure.Forest.rowDecomp_𝔘_eq line 227 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, Eq, 𝔓, TileStructure.Forest.𝔘, TileStructure.Row.toForest and 2 more
Proof uses: rfl
26 instances, coercions and auxiliary constants left out.
lemma TileStructure.Forest.mem_rowDecomp_iff_mem_rowDecomp_𝔘 line 230 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, 𝔓, Iff, Membership.mem, TileStructure.Row and 2 more
Proof uses: Iff.rfl
29 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma TileStructure.Forest.stackSize_remainder_ge_one_of_exists line 233 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, Exists, 𝔓, And, Membership.mem and 12 more
Proof uses: Trans.trans, Eq, Singleton.singleton, Eq.mpr, Finset.sum, Finset.filter, Classical.propDecidable, Finset.univ, Set.indicator, id, congrArg, stackSize.eq_1, Finset.sum_eq_single_of_mem, Finset, propext, Finset.mem_filter_univ, Iff.mpr, Set.mem_singleton_iff, rfl, Ne and 10 more
61 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
lemma TileStructure.Forest.remainder_stackSize_le line 251 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, LE.le, stackSize, SDiff.sdiff, 𝔓 and 8 more
Proof uses: Nat.recAux, Eq.mpr, id, Eq, congr, congrArg, congrFun', Eq.trans, EmptyCollection.emptyCollection, funext, False, Set.iUnion_congr_Prop, Iff.of_eq, Eq.refl, Set.iUnion_of_empty, Set.iUnion_empty, Set.sdiff_empty, tsub_zero, TileStructure.Forest.stackSize_le', dite and 70 more
115 instances, coercions and auxiliary constants left out.

Tactic trace: 62 steps
Open to load the checked before-and-after goal states.
lemma TileStructure.Forest.biUnion_rowDecomp Part of Lemma 7.7.1 line 317 source
Source documentation
Part of Lemma 7.7.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, Eq, 𝔓, Set.iUnion, LT.lt and 5 more
Proof uses: subset_antisymm, Eq.mpr, LE.le, id, Eq.trans, forall_congr, TileStructure.Forest.rowDecomp_𝔘_subset_forest, SDiff.sdiff, EmptyCollection.emptyCollection, congrArg, Eq.symm, propext, Set.sdiff_eq_empty, eq_empty_of_forall_stackSize_zero, Nat.eq_zero_of_le_zero, stackSize, Eq.rec, HSub.hSub, TileStructure.Forest.remainder_stackSize_le, Nat.sub_self
53 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
lemma biUnion_rowDecomp : ⋃ j < 2 ^ n, t.rowDecomp j = (t : Set (𝔓 X)) := by
…
```
Mentions: 𝔓
lemma TileStructure.Forest.pairwiseDisjoint_rowDecomp Part of Lemma 7.7.1 line 326 source
Source documentation
Part of Lemma 7.7.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, 𝔓, Set.Iio, HPow.hPow and 4 more
Proof uses: Membership.mem, Ne, Eq.mpr, Function.onFun, Disjoint, id, Eq, congrArg, Function.onFun_apply, LE.le, Inter.inter, EmptyCollection.emptyCollection, propext, Set.disjoint_iff, LT.lt, Not, Or, Classical.em, Eq.trans, False and 13 more
80 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
```
lemma pairwiseDisjoint_rowDecomp :
    (Iio (2 ^ n)).PairwiseDisjoint (rowDecomp t · : ℕ → Set (𝔓 X)) := by
…
```
Mentions: TileStructure.Forest.rowDecomp, 𝔓
lemma TileStructure.Forest.rowDecomp_apply line 343 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, 𝔓, Eq, TileStructure.Forest.𝔗, TileStructure.Row.toForest and 1 more
Proof uses: rfl
26 instances, coercions and auxiliary constants left out.
def TileStructure.Forest.carlesonRowSum The definition of T_{ℜ_j}f(x), defined above Lemma 7.7.2 line 347 source
Source documentation
The definition of T_{ℜ_j}f(x), defined above Lemma 7.7.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
Proof uses: Finset.sum, 𝔓, Finset.filter, Membership.mem, TileStructure.Row, TileStructure.Forest.rowDecomp, Classical.propDecidable, Finset.univ, carlesonSum, TileStructure.Forest.𝔗
28 instances, coercions and auxiliary constants left out.
```
def carlesonRowSum (t : Forest X n) (j : ℕ) (f : X → ℂ) (x : X) : ℂ :=
…
```
Mentions: TileStructure.Forest
def TileStructure.Forest.adjointCarlesonRowSum The definition of T_{ℜ_j}*f(x), defined above Lemma 7.7.2 line 352 source
Source documentation
The definition of T_{ℜ_j}*f(x), defined above Lemma 7.7.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
Proof uses: Finset.sum, 𝔓, Finset.filter, Membership.mem, TileStructure.Row, TileStructure.Forest.rowDecomp, Classical.propDecidable, Finset.univ, adjointCarlesonSum, TileStructure.Forest.𝔗
28 instances, coercions and auxiliary constants left out.
```
def adjointCarlesonRowSum (t : Forest X n) (j : ℕ) (f : X → ℂ) (x : X) : ℂ :=
…
```
Mentions: TileStructure.Forest
lemma TileStructure.Forest.adjointCarlesonRowSum_adjoint adjointCarlesonRowSum is the adjoint of carlesonRowSum line 356 source
Source documentation
adjointCarlesonRowSum is the adjoint of carlesonRowSum.

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, MeasureTheory.integral and 5 more
Proof uses: Trans.trans, Finset.sum, 𝔓, Finset.filter, Membership.mem, TileStructure.Row, TileStructure.Forest.rowDecomp, Classical.propDecidable, Finset.univ, adjointCarlesonSum, TileStructure.Forest.𝔗, carlesonSum, id, Eq.mpr, congr, congrArg, funext, Finset.sum_congr, Eq.refl, Finset and 26 more
137 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
```
lemma adjointCarlesonRowSum_adjoint
    (hf : BoundedCompactSupport f) (hg : BoundedCompactSupport g) (j : ℕ) :
    ∫ x, conj (g x) * carlesonRowSum t j f x = ∫ x, conj (adjointCarlesonRowSum t j g x) * f x := by
…
```
Mentions: g, TileStructure.Forest.carlesonRowSum, TileStructure.Forest.adjointCarlesonRowSum
lemma TileStructure.Forest.row_bound_common Common proof structure for the two parts of Lemma 7.7.2 line 374 source
Source documentation
Common proof structure for the two parts of Lemma 7.7.2.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, TileStructure.Forest, MeasureTheory.BoundedCompactSupport, MeasureTheory.MeasureSpace.volume, MeasurableSet, ENNReal and 13 more
Proof uses: Eq.mpr, HPow.hPow, id, Eq, congrArg, Eq.symm, propext, ENNReal.rpow_le_rpow_iff, LT.lt, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_zero, Mathlib.Meta.NormNum.isNat_natCast, Eq.refl, Bool, Bool.false, ENNReal.rpow_natCast, MeasureTheory.BoundedCompactSupport.adjointCarlesonSum, MeasureTheory.BoundedCompactSupport.indicator, GridStructure.coeGrid_measurable and 70 more
220 instances, coercions and auxiliary constants left out.

Tactic trace: 39 steps
Open to load the checked before-and-after goal states.
```
lemma row_bound_common (hg : BoundedCompactSupport g) {A : Set X} (mA : MeasurableSet A) {C : ℝ≥0∞}
    (hC : ∀ u ∈ t.rowDecomp j,
      eLpNorm (A.indicator (adjointCarlesonSum (t u) ((𝓘 u : Set X).indicator g))) 2 ≤
      C * eLpNorm ((𝓘 u : Set X).indicator g) 2) :
    eLpNorm (A.indicator (adjointCarlesonRowSum t j g)) 2 ≤ C * eLpNorm g 2 := by
…
```
Mentions: g, A, adjointCarlesonSum, 𝓘, TileStructure.Forest.adjointCarlesonRowSum
lemma TileStructure.Forest.le_C7_7_2_1 line 425 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, NNReal, HMul.hMul, TileStructure.Forest.C7_3_1_1, HPow.hPow, Real, HAdd.hAdd, HSub.hSub, Inv.inv, TileStructure.Forest.C7_7_2_1
Proof uses: Eq.mpr, id, Eq, congrArg, sub_add_eq_add_sub, Neg.neg, sub_eq_add_neg, NNReal.rpow_add, two_ne_zero, NNReal.mul_rpow, HDiv.hDiv, Eq.rec, Eq.refl, Eq.trans, Eq.symm, NNReal.rpow_mul, div_eq_mul_inv, neg_div, 𝕔, TileStructure.Forest.C7_7_2_1_def and 130 more
187 instances, coercions and auxiliary constants left out.

Tactic trace: 21 steps
Open to load the checked before-and-after goal states.
lemma TileStructure.Forest.le_C7_7_2_2 line 450 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, NNReal, HMul.hMul, TileStructure.Forest.C7_3_1_2, HPow.hPow, Real, HAdd.hAdd, HSub.hSub, Inv.inv, TileStructure.Forest.C7_7_2_2
Proof uses: Eq.mpr, id, Eq, congrArg, sub_add_eq_add_sub, Neg.neg, sub_eq_add_neg, NNReal.rpow_add, two_ne_zero, NNReal.mul_rpow, HDiv.hDiv, Eq.rec, Eq.refl, Eq.trans, Eq.symm, NNReal.rpow_mul, div_eq_mul_inv, neg_div, 𝕔, TileStructure.Forest.C7_7_2_2_def and 130 more
187 instances, coercions and auxiliary constants left out.

Tactic trace: 21 steps
Open to load the checked before-and-after goal states.
lemma TileStructure.Forest.row_bound line 469 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, TileStructure.Forest, MeasureTheory.BoundedCompactSupport, MeasureTheory.MeasureSpace.volume, LE.le, Function.support and 6 more
Proof uses: Eq.mpr, Set.indicator, Set.univ, id, Eq, congrArg, Eq.symm, Set.indicator_univ, TileStructure.Forest.row_bound_common, MeasurableSet.univ, 𝔓, Membership.mem, TileStructure.Row, TileStructure.Forest.rowDecomp, adjointCarlesonSum, TileStructure.Forest.𝔗, 𝓘, Trans.trans, TileStructure.Forest.C7_3_1_1, HPow.hPow and 39 more
155 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
lemma TileStructure.Forest.indicator_row_bound line 488 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, TileStructure.Forest, MeasureTheory.BoundedCompactSupport, MeasureTheory.MeasureSpace.volume, LE.le, Function.support and 14 more
Proof uses: TileStructure.Forest.row_bound_common, ProofData.measurableSet_F, TileStructure.Row, TileStructure.Forest.rowDecomp, Trans.trans, adjointCarlesonSum, 𝓘, TileStructure.Forest.C7_3_1_2, HAdd.hAdd, HSub.hSub, dens₁, TileStructure.Forest.indicator_adjoint_tree_estimate, MeasureTheory.BoundedCompactSupport.indicator, GridStructure.coeGrid_measurable, Eq.mpr, Inter.inter, id, Eq, congrArg, Set.support_indicator and 41 more
181 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
lemma TileStructure.Forest.row_correlation_aux line 510 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, TileStructure.Forest, MeasureTheory.BoundedCompactSupport, MeasureTheory.MeasureSpace.volume, LE.le, Function.support and 19 more
Proof uses: Finset, Eq.mpr, id, Eq, congrArg, rfl, Trans.trans, MeasureTheory.lintegral, MeasureTheory.Measure.restrict, Set.iUnion, eq_of_heq, outParam, HPow, HEq, Eq.refl, HEq.refl, Eq.symm, Finset.sum_congr, ENNReal.rpow_natCast, ENorm.enorm and 69 more
185 instances, coercions and auxiliary constants left out.

Tactic trace: 38 steps
Open to load the checked before-and-after goal states.
lemma TileStructure.Forest.row_correlation Lemma 7.7.3 line 561 source
Source documentation
Lemma 7.7.3.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, TileStructure.Forest, LT.lt, HPow.hPow, OfNat.ofNat, Ne and 13 more
Proof uses: Finset, Prod, 𝔓, SProd.sprod, Finset.filter, Membership.mem, TileStructure.Row, TileStructure.Forest.rowDecomp, Classical.propDecidable, Finset.univ, Set.indicator, Inter.inter, 𝓘, Prod.fst, Prod.snd, TileStructure.Forest.adjointBoundaryOperator, Finset.sum, Inv.inv, TileStructure.Forest.C7_4_3, id and 82 more
215 instances, coercions and auxiliary constants left out.

Tactic trace: 42 steps
Open to load the checked before-and-after goal states.
```
lemma row_correlation (lj : j < 2 ^ n) (lj' : j' < 2 ^ n) (hn : j ≠ j')
    (hf₁ : BoundedCompactSupport f₁) (nf₁ : f₁.support ⊆ G)
    (hf₂ : BoundedCompactSupport f₂) (nf₂ : f₂.support ⊆ G) :
    ‖∫ x, adjointCarlesonRowSum t j f₁ x * conj (adjointCarlesonRowSum t j' f₂ x)‖ₑ ≤
    C7_7_3 a n * eLpNorm f₁ 2 volume * eLpNorm f₂ 2 volume := by
…
```
Mentions: TileStructure.Forest.adjointCarlesonRowSum
def TileStructure.Forest.rowSupport The definition of Eⱼ defined above Lemma 7.7.4 line 630 source
Source documentation
The definition of Eⱼ defined above Lemma 7.7.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
Proof uses: Set.iUnion, 𝔓, Membership.mem, TileStructure.Row, TileStructure.Forest.rowDecomp, TileStructure.Forest.𝔗, E
27 instances, coercions and auxiliary constants left out.
```
def rowSupport (j : ℕ) : Set X := ⋃ (u ∈ rowDecomp t j) (p ∈ t u), E p
```
Mentions: TileStructure.Forest.rowDecomp, E
lemma TileStructure.Forest.disjoint_impl line 632 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, 𝔓, Disjoint, FunctionDistances.Θ, TileStructure.Ω, E
Proof uses: Eq.mpr, LE.le, Inter.inter, EmptyCollection.emptyCollection, id, Eq, implies_congr, Membership.mem, MeasureTheory.SimpleFunc, And.intro, Q_mem_Ω, And.left, And.right
69 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma TileStructure.Forest.disjoint_of_ne_of_mem line 637 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, 𝔓, Ne, Membership.mem, TileStructure.Row and 4 more
Proof uses: LE.le, 𝔰, Not, Or, Classical.em, Iff.mp, not_imp_self, TileStructure.Forest.disjoint_impl, Exists, FunctionDistances.Θ, TileStructure.Ω, Eq.mp, Eq.trans, congrArg, Inter.inter, EmptyCollection.emptyCollection, forall_congr, And, False, implies_congr and 61 more
129 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
lemma TileStructure.Forest.measurableSet_rowSupport line 667 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, MeasurableSet, TileStructure.Forest.rowSupport
Proof uses: Set.Finite.measurableSet_biUnion, 𝔓, Set.iUnion, Membership.mem, TileStructure.Forest.𝔗, E, TileStructure.Forest.𝔘, TileStructure.Row.toForest, TileStructure.Forest.rowDecomp, Set.toFinite, measurableSet_E
33 instances, coercions and auxiliary constants left out.
lemma TileStructure.Forest.pairwiseDisjoint_rowSupport Lemma 7.7.4 line 672 source
Source documentation
Lemma 7.7.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, Set.PairwiseDisjoint, Set.Iio, HPow.hPow, OfNat.ofNat and 1 more
Proof uses: Membership.mem, Ne, Disjoint, 𝔓, TileStructure.Forest.𝔘, TileStructure.Row.toForest, TileStructure.Forest.rowDecomp, TileStructure.Forest.pairwiseDisjoint_rowDecomp, id, Function.onFun, Eq.mpr, Set.iUnion, HMul.hMul, 𝕔, TileStructure.Row, TileStructure.Forest.𝔗, E, Eq, Eq.trans, forall_congr and 4 more
63 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
lemma pairwiseDisjoint_rowSupport : (Iio (2 ^ n)).PairwiseDisjoint (rowSupport t) := by
…
```
Mentions: TileStructure.Forest.rowSupport
lemma TileStructure.Forest.forest_operator_g_prelude line 685 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, TileStructure.Forest, Measurable, LE.le, Norm.norm, Set.indicator and 18 more
Proof uses: MeasureTheory.BoundedCompactSupport, bcs_of_measurable_of_le_indicator_f, bcs_of_measurable_of_le_indicator_g, Trans.trans, MeasureTheory.lintegral, Eq, ENorm, Eq.rec, Eq.refl, Eq.mpr, id, congrArg, Eq.symm, MeasureTheory.integral_finsetSum, Finset, MeasureTheory.BoundedCompactSupport.integrable_fun_mul, MeasureTheory.BoundedCompactSupport.starRingEnd, MeasureTheory.BoundedCompactSupport.integrable, MeasureTheory.BoundedCompactSupport.carlesonSum, congr and 28 more
189 instances, coercions and auxiliary constants left out.

Tactic trace: 25 steps
Open to load the checked before-and-after goal states.
lemma TileStructure.Forest.adjointCarlesonRowSum_rowSupport line 711 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, Eq, TileStructure.Forest.adjointCarlesonRowSum, Set.indicator, TileStructure.Forest.rowSupport
Proof uses: funext, id, Finset.sum, 𝔓, Finset.filter, Membership.mem, TileStructure.Row, TileStructure.Forest.rowDecomp, Classical.propDecidable, Finset.univ, adjointCarlesonSum, TileStructure.Forest.𝔗, Finset.sum_congr, adjointCarleson, Eq.refl, Finset, MeasureTheory.setIntegral_congr_ae, HMul.hMul, RingHom, starRingEnd and 29 more
59 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
def TileStructure.Forest.G2_0_4 The constant on the g side of Proposition 2.0.4 line 721 source
Source documentation
The constant on the g side of Proposition 2.0.4. Has value 2 ^ (440 * a ^ 3) in the blueprint.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NNReal
Proof uses: HMul.hMul, HPow.hPow, OfNat.ofNat, HAdd.hAdd, 𝕔, HDiv.hDiv, Real, Neg.neg
27 instances, coercions and auxiliary constants left out.
```
def G2_0_4 (a n : ℕ) : ℝ≥0 := 2 ^ ((3 * 𝕔 + 15 + 5 * (𝕔 / 4)) * a ^ 3) * 2 ^ (-(n / 2 : ℝ))
```
lemma TileStructure.Forest.le_sq_G2_0_4 line 723 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, NNReal, HAdd.hAdd, HPow.hPow, TileStructure.Forest.C7_7_2_1, HMul.hMul, TileStructure.Forest.C7_7_3, TileStructure.Forest.G2_0_4
Proof uses: Eq.mpr, 𝕔, HDiv.hDiv, Real, Neg.neg, id, Eq, congr, congrArg, Eq.trans, congrFun', TileStructure.Forest.C7_7_2_1_def, mul_pow, TileStructure.Forest.C7_4_3, TileStructure.Forest.C7_4_4, TileStructure.Forest.C7_7_3_def, TileStructure.Forest.C7_4_3_def, TileStructure.Forest.C7_4_4_def, NNReal.rpow_le_rpow_of_exponent_le, Mathlib.Meta.NormNum.isNat_le_true and 104 more
156 instances, coercions and auxiliary constants left out.

Tactic trace: 24 steps
Open to load the checked before-and-after goal states.
lemma TileStructure.Forest.support_subset_of_norm_le_indicator line 745 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Complex, Real, Set, LE.le, Norm.norm, Set.indicator, Function.support
Proof uses: Membership.mem, Mathlib.Tactic.Contrapose.contrapose₁, Not, Eq.mpr, Eq, OfNat.ofNat, id, Eq.trans, congrArg, Eq.mp, Zero, Set.indicator_of_notMem
22 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma TileStructure.Forest.forest_operator_g_main line 755 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, TileStructure.Forest, Measurable, LE.le, Norm.norm, Set.indicator and 15 more
Proof uses: MeasureTheory.BoundedCompactSupport, bcs_of_measurable_of_le_indicator_g, TileStructure.Forest.adjointCarlesonRowSum, TileStructure.Forest.rowSupport, MeasureTheory.BoundedCompactSupport.indicator, TileStructure.Forest.measurableSet_rowSupport, id, MeasureTheory.BoundedCompactSupport.finset_sum, TileStructure.Row, TileStructure.Forest.rowDecomp, Finset, MeasureTheory.BoundedCompactSupport.adjointCarlesonSum, Trans.trans, HAdd.hAdd, TileStructure.Forest.C7_7_2_1, TileStructure.Forest.C7_7_3, Finset.range, Ne, Eq, ENorm.enorm and 101 more
232 instances, coercions and auxiliary constants left out.

Tactic trace: 61 steps
Open to load the checked before-and-after goal states.
lemma TileStructure.Forest.forest_operator_g The g side of Proposition 2.0.4 line 826 source
Source documentation
The g side of Proposition 2.0.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, Measurable, LE.le, Norm.norm, Set.indicator and 18 more
Proof uses: Trans.trans, adjointCarlesonSum, TileStructure.Forest.forest_operator_g_prelude, Eq.mpr, id, Eq, congrArg, mul_comm, mul_assoc, mul_le_mul', le_refl, HPow.hPow, Eq.symm, propext, ENNReal.rpow_le_rpow_iff, LT.lt, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_zero, Mathlib.Meta.NormNum.isNat_natCast and 5 more
153 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma forest_operator_g (t : Forest X n)
    (hf : Measurable f) (h2f : ∀ x, ‖f x‖ ≤ F.indicator 1 x)
    (hg : Measurable g) (h2g : ∀ x, ‖g x‖ ≤ G.indicator 1 x) :
    ‖∫ x, conj (g x) * ∑ u with u ∈ t, carlesonSum (t u) f x‖ₑ ≤
    G2_0_4 a n * eLpNorm f 2 volume * eLpNorm g 2 volume := by
…
```
Mentions: TileStructure.Forest, g, carlesonSum, TileStructure.Forest.G2_0_4
lemma TileStructure.Forest.carlesonRowSum_rowSupport line 839 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, Eq, TileStructure.Forest.carlesonRowSum, Set.indicator, TileStructure.Forest.rowSupport
Proof uses: Eq.symm, Eq.mpr, LE.le, Function.support, id, congrArg, propext, Set.indicator_eq_self, Not, Membership.mem, OfNat.ofNat, Function.support_subset_iff', Finset.sum_eq_zero, 𝔓, Finset.filter, TileStructure.Row, TileStructure.Forest.rowDecomp, Classical.propDecidable, Finset.univ, carlesonSum and 28 more
58 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma TileStructure.Forest.forest_operator_f_prelude line 848 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, TileStructure.Forest, Measurable, LE.le, Norm.norm, Set.indicator and 17 more
Proof uses: MeasureTheory.BoundedCompactSupport, bcs_of_measurable_of_le_indicator_f, bcs_of_measurable_of_le_indicator_g, Trans.trans, MeasureTheory.lintegral, Eq, Eq.mpr, id, Eq.rec, Eq.refl, funext, Eq.trans, congrArg, Eq.symm, RCLike.enorm_conj, enorm_mul, MeasureTheory.enorm_integral_le_lintegral_enorm, eq_of_heq, MeasurableSpace, MeasureTheory.Measure and 32 more
184 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
lemma TileStructure.Forest.forest_operator_f_inner https://leanprover.zulipchat.com/#narrow/channel/442935-Carleson/topic/Problems.20in.20the.20forest.20operator.20proposition/near/522771057 line 873 source
Source documentation
https://leanprover.zulipchat.com/#narrow/channel/442935-Carleson/topic/Problems.20in.20the.20forest.20operator.20proposition/near/522771057

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, TileStructure.Forest, Measurable, LE.le, Norm.norm, Set.indicator and 14 more
Proof uses: MeasureTheory.BoundedCompactSupport, bcs_of_measurable_of_le_indicator_f, Eq.mpr, id, Eq, congrArg, rfl, MeasureTheory.BoundedCompactSupport.indicator, Finset.sum, Finset.filter, TileStructure.Row, TileStructure.Forest.rowDecomp, Classical.propDecidable, Finset.univ, carlesonSum, MeasureTheory.BoundedCompactSupport.finset_sum, Finset, MeasureTheory.BoundedCompactSupport.carlesonSum, ProofData.measurableSet_G, Trans.trans and 77 more
239 instances, coercions and auxiliary constants left out.

Tactic trace: 37 steps
Open to load the checked before-and-after goal states.
```
lemma forest_operator_f_inner (hf : Measurable f) (h2f : ∀ x, ‖f x‖ ≤ F.indicator 1 x) :
    eLpNorm (G.indicator (carlesonRowSum t j f)) 2 ≤
    C7_7_2_2 a n * dens₂ (⋃ u ∈ t, t u) ^ (2 : ℝ)⁻¹ * eLpNorm f 2 := by
…
```
Mentions: TileStructure.Forest.carlesonRowSum, dens₂
def TileStructure.Forest.C2_0_4_aux The constant in the f side of Proposition 2.0.4 line 915 source
Source documentation
The constant in the f side of Proposition 2.0.4. Has value 2 ^ (283 * a ^ 3) in the blueprint.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NNReal
Proof uses: HPow.hPow, OfNat.ofNat, HMul.hMul, HAdd.hAdd, 𝕔, HDiv.hDiv
19 instances, coercions and auxiliary constants left out.
```
def C2_0_4_aux (a : ℕ) : ℝ≥0 := 2 ^ ((2 * 𝕔 + 8 + 𝕔 / 2 + 𝕔 / 4) * a ^ 3)
…
```
lemma TileStructure.Forest.forest_operator_f_main line 918 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, TileStructure.Forest, Measurable, LE.le, Norm.norm, Set.indicator and 18 more
Proof uses: MeasureTheory.BoundedCompactSupport, bcs_of_measurable_of_le_indicator_f, TileStructure.Forest.rowSupport, TileStructure.Forest.carlesonRowSum, MeasureTheory.BoundedCompactSupport.indicator, TileStructure.Row, TileStructure.Forest.rowDecomp, MeasureTheory.BoundedCompactSupport.finset_sum, Finset, MeasureTheory.BoundedCompactSupport.carlesonSum, TileStructure.Forest.measurableSet_rowSupport, ProofData.measurableSet_G, Trans.trans, Eq, Finset.range, TileStructure.Forest.C7_7_2_2, HAdd.hAdd, Ne, ENorm.enorm, MeasureTheory.integral and 124 more
307 instances, coercions and auxiliary constants left out.

Tactic trace: 54 steps
Open to load the checked before-and-after goal states.
lemma TileStructure.Forest.forest_operator_f The f side of Proposition 2.0.4 line 987 source
Source documentation
The f side of Proposition 2.0.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, Measurable, LE.le, Norm.norm, Set.indicator and 22 more
Proof uses: Trans.trans, TileStructure.Forest.forest_operator_f_prelude, Eq.mpr, id, Eq, congrArg, Eq.symm, mul_rotate, mul_assoc, mul_le_mul', le_refl, propext, ENNReal.rpow_le_rpow_iff, LT.lt, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_zero, Mathlib.Meta.NormNum.isNat_natCast, Eq.refl, Bool and 3 more
158 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma forest_operator_f (t : Forest X n)
    (hf : Measurable f) (h2f : ∀ x, ‖f x‖ ≤ F.indicator 1 x)
    (hg : Measurable g) (h2g : ∀ x, ‖g x‖ ≤ G.indicator 1 x) :
    ‖∫ x, conj (g x) * ∑ u with u ∈ t, carlesonSum (t u) f x‖ₑ ≤
    C2_0_4_aux a * dens₂ (⋃ u ∈ t, t u) ^ (2 : ℝ)⁻¹ *
    eLpNorm f 2 volume * eLpNorm g 2 volume := by
…
```
Mentions: TileStructure.Forest, g, carlesonSum, TileStructure.Forest.C2_0_4_aux, dens₂
theorem forest_operator line 1014 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, TileStructure.Forest, Measurable, LE.le, Norm.norm, Set.indicator and 23 more
Proof uses: TileStructure.Forest.G2_0_4, TileStructure.Forest.forest_operator_g, TileStructure.Forest.C2_0_4_aux, TileStructure.Forest.forest_operator_f, Eq, LT.lt, Or, LE.le.eq_or_lt, q_le_two, Eq.mpr, id, congrArg, sub_self, ENNReal.rpow_zero, mul_one, C2_0_4_base, HDiv.hDiv, Neg.neg, C2_0_4_def, HAdd.hAdd and 145 more
280 instances, coercions and auxiliary constants left out.

Tactic trace: 41 steps
Open to load the checked before-and-after goal states.
theorem forest_operator' Version of the forest operator theorem, but controlling the integral of the norm instead of the integral of the function multiplied by another function line 1066 source
Source documentation
Version of the forest operator theorem, but controlling the integral of the norm instead of the integral of the function multiplied by another function.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, TileStructure.Forest, Measurable, LE.le, Norm.norm, Set.indicator and 25 more
Proof uses: MeasureTheory.BoundedCompactSupport, bcs_of_measurable_of_le_indicator_f, Eq.mpr, MeasureTheory.integral, RingHom, starRingEnd, id, Eq, congrArg, Eq.symm, enorm_integral_starRingEnd_mul_eq_lintegral_enorm, MeasureTheory.BoundedCompactSupport.integrable, MeasureTheory.BoundedCompactSupport.finset_sum, Finset, MeasureTheory.BoundedCompactSupport.restrict, MeasureTheory.BoundedCompactSupport.carlesonSum, MeasureTheory.integral_indicator, congr, funext, congrFun' and 90 more
307 instances, coercions and auxiliary constants left out.

Tactic trace: 45 steps
Open to load the checked before-and-after goal states.
```
theorem forest_operator' {n : ℕ} (𝔉 : Forest X n) {f : X → ℂ} {A : Set X}
    (hf : Measurable f) (h2f : ∀ x, ‖f x‖ ≤ F.indicator 1 x) (hA : MeasurableSet A) (sA : A ⊆ G) :
    ∫⁻ x in A, ‖∑ u with u ∈ 𝔉, carlesonSum (𝔉 u) f x‖ₑ ≤
    C2_0_4 a q n * (dens₂ (⋃ u ∈ 𝔉, 𝔉 u)) ^ (q⁻¹ - 2⁻¹) *
    eLpNorm f 2 volume * (volume A) ^ (1/2 : ℝ) := by
…
```
Mentions: A, carlesonSum, dens₂
theorem forest_operator_le_volume Documented declaration: forest_operator_le_volume line 1108 source
Source documentation
Version of the forest operator theorem, but controlling the integral of the norm instead of the integral of the function multiplied by another function, and with the upper bound in terms of volume F and volume 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, TileStructure.Forest, Measurable, LE.le, Norm.norm, Set.indicator and 24 more
Proof uses: LE.le.trans, MeasureTheory.eLpNorm, forest_operator', mul_le_mul', le_refl, Trans.trans, MeasureTheory.eLpNorm_mono, le_abs_self, Eq.mpr, ENNReal.toReal, id, Eq, congrArg, MeasureTheory.eLpNorm_indicator_const, ProofData.measurableSet_F, Mathlib.Meta.NormNum.isNat_eq_false, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Nat.cast_zero and 18 more
162 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
theorem forest_operator_le_volume {n : ℕ} (𝔉 : Forest X n) {f : X → ℂ} {A : Set X}
    (hf : Measurable f) (h2f : ∀ x, ‖f x‖ ≤ F.indicator 1 x) (hA : MeasurableSet A) (sA : A ⊆ G) :
    ∫⁻ x in A, ‖∑ u with u ∈ 𝔉, carlesonSum (𝔉 u) f x‖ₑ ≤
    C2_0_4 a q n * (dens₂ (⋃ u ∈ 𝔉, 𝔉 u)) ^ (q⁻¹ - 2⁻¹) *
    (volume F) ^ (1/2 : ℝ) * (volume A) ^ (1/2 : ℝ) := by
…
```
Mentions: A, carlesonSum, dens₂