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

74 declarations, 0 contain sorry, 0 declared as axioms

Section 7.5

Imports (4)

Imported by 2 files

def TileStructure.Forest.𝓙₅ The definition 𝓙' at the start of Section 7.5.1 line 29 source
Source documentation
The definition 𝓙' at the start of Section 7.5.1. We use a different notation to distinguish it from the 𝓙' used in Section 7.6

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, TileStructure.Forest, 𝔓, Grid
Proof uses: Inter.inter, TileStructure.Forest.𝓙, TileStructure.Forest.𝔖₀, Set.Iic, 𝓘
31 instances, coercions and auxiliary constants left out.
```
def 𝓙₅ : Set (Grid X) := 𝓙 (𝔖₀ t u₁ u₂) ∩ Iic (𝓘 u₁)
```
Mentions: Grid, TileStructure.Forest.𝓙, TileStructure.Forest.𝔖₀, 𝓘
def TileStructure.Forest.χtilde The definition of χ-tilde, defined in the proof of Lemma 7.5.2 line 32 source
Source documentation
The definition of χ-tilde, defined in the proof of Lemma 7.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, Grid, 𝔓
Proof uses: Set.indicator, 𝓘, Real.toNNReal, HSub.hSub, OfNat.ofNat, HMul.hMul, HPow.hPow, Neg.neg, s, Dist.dist, c
43 instances, coercions and auxiliary constants left out.
```
def χtilde (J : Grid X) (u₁ : 𝔓 X) : X → ℝ≥0 :=
…
```
Mentions: Grid, 𝔓
lemma TileStructure.Forest.χtilde_pos_iff line 35 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, Iff, LT.lt, OfNat.ofNat and 9 more
Proof uses: LE.le, one_le_realD, Eq.mpr, Set.indicator, Real.toNNReal, HSub.hSub, Neg.neg, Dist.dist, id, Eq, congrArg, TileStructure.Forest.χtilde.eq_1, dite, Classical.propDecidable, Set.indicator_of_mem, propext, Real.toNNReal_pos, sub_pos, HAdd.hAdd, Inv.inv and 24 more
147 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
lemma TileStructure.Forest.χtilde_le_eight line 48 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, LE.le, TileStructure.Forest.χtilde, OfNat.ofNat
Proof uses: id, Set.indicator_le, 𝓘, Real.toNNReal, HSub.hSub, HMul.hMul, HPow.hPow, Neg.neg, s, Dist.dist, c, Membership.mem, Eq.mpr, Eq, congrArg, propext, Real.toNNReal_le_iff_le_coe, NNReal.coe_ofNat, sub_le_self_iff, mul_nonneg and 3 more
94 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma TileStructure.Forest.four_lt_χtilde line 53 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, Membership.mem, 𝓘, LT.lt and 2 more
Proof uses: LE.le, one_le_realD, id, Eq.mpr, Set.indicator, Real.toNNReal, HSub.hSub, HMul.hMul, HPow.hPow, Neg.neg, s, Dist.dist, c, Eq, congrArg, Zero, Set.indicator_of_mem, Mathlib.Meta.NormNum.isNat_eq_true, Mathlib.Meta.NormNum.instAddMonoidWithOne, Mathlib.Meta.NormNum.IsInt.to_isNat and 20 more
117 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma TileStructure.Forest.dist_χtilde_le line 59 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, Membership.mem, 𝓘, LE.le and 5 more
Proof uses: Trans.trans, Norm.norm, HSub.hSub, c, Eq, OfNat.ofNat, HMul.hMul, Neg.neg, Eq.mpr, Set.indicator, Real.toNNReal, id, congrArg, TileStructure.Forest.χtilde.eq_1, Set.indicator_of_mem, norm_sup_sub_sup_le_norm, sub_sub_sub_cancel_left, Eq.symm, mul_sub, Inv.inv and 21 more
144 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma TileStructure.Forest.stronglyMeasurable_χtilde line 71 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, MeasureTheory.StronglyMeasurable, TileStructure.Forest.χtilde
Proof uses: Measurable.stronglyMeasurable, Set.indicator, 𝓘, Real.toNNReal, HSub.hSub, OfNat.ofNat, HMul.hMul, HPow.hPow, Neg.neg, s, Dist.dist, id, c, Measurable.indicator, Measurable.real_toNNReal, Measurable.const_sub, Measurable.const_mul, Measurable.dist, measurable_id, measurable_const and 1 more
79 instances, coercions and auxiliary constants left out.
def TileStructure.Forest.χ The definition of χ, defined in the proof of Lemma 7.5.2 line 78 source
Source documentation
The definition of χ, defined in the proof of Lemma 7.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, TileStructure.Forest, 𝔓, Grid
Proof uses: HDiv.hDiv, TileStructure.Forest.χtilde, Finset.sum, Set.toFinset, TileStructure.Forest.𝓙₅, Membership.mem, Classical.propDecidable
34 instances, coercions and auxiliary constants left out.
```
def χ (J : Grid X) (x : X) : ℝ≥0 :=
…
```
Mentions: Grid
lemma TileStructure.Forest.stronglyMeasurable_χ line 81 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, TileStructure.Forest, 𝔓, Grid, MeasureTheory.StronglyMeasurable, TileStructure.Forest.χ
Proof uses: Measurable.stronglyMeasurable, HDiv.hDiv, TileStructure.Forest.χtilde, Finset.sum, Set.toFinset, TileStructure.Forest.𝓙₅, Membership.mem, Classical.propDecidable, Measurable.div, MeasureTheory.StronglyMeasurable.measurable, TileStructure.Forest.stronglyMeasurable_χtilde, Finset.measurable_sum, Finset
77 instances, coercions and auxiliary constants left out.
def TileStructure.Forest.holderFunction The definition of h_J, defined in the proof of Section 7.5.2 line 89 source
Source documentation
The definition of h_J, defined in the proof of Section 7.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, TileStructure.Forest, 𝔓, Grid
Proof uses: HMul.hMul, TileStructure.Forest.χ, Complex.exp, Complex.I, FunctionDistances.Θ, PreTileStructure.𝒬, adjointCarlesonSum, TileStructure.Forest.𝔗, RingHom, starRingEnd, Inter.inter, TileStructure.Forest.𝔖₀
43 instances, coercions and auxiliary constants left out.
```
def holderFunction (f₁ f₂ : X → ℂ) (J : Grid X) (x : X) : ℂ :=
…
```
Mentions: Grid
lemma TileStructure.Forest.IF_subset_THEN_not_disjoint line 95 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, LE.le, Not, Disjoint
Proof uses: Eq.mpr, id, Eq, congrArg, propext, disjoint_comm, EmptyCollection.emptyCollection, Set.disjoint_of_subset_iff_left_eq_empty, Ne, Eq.symm, Ne.eq_1, Set.Nonempty, Set.nonempty_iff_ne_empty, Grid.nonempty
59 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma TileStructure.Forest.IF_disjoint_with_ball_THEN_distance_bigger_than_radius line 100 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MetricSpace, Real, Set, Membership.mem, Disjoint, Metric.ball, GE.ge, Dist.dist
Proof uses: Decidable.byContradiction, Not, Iff.mp, EmptyCollection.emptyCollection, False, Set.mem_empty_iff_false, Eq.mpr, Inter.inter, id, Eq, congrArg, Eq.symm, Eq.mp, Set.inter_comm, propext, Set.disjoint_iff_inter_eq_empty, Iff.mpr, And, Set.mem_inter_iff, And.intro and 2 more
41 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma TileStructure.Forest.dist_triangle5 line 111 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MetricSpace, LE.le, Real, Dist.dist, HAdd.hAdd
Proof uses: Trans.trans, dist_triangle, add_le_add_left
18 instances, coercions and auxiliary constants left out.
lemma TileStructure.Forest.𝓘_subset_iUnion_𝓙_𝔖₀ line 119 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, 𝓘, Set.iUnion and 4 more
Proof uses: Eq.mpr, id, Eq, congrArg, TileStructure.Forest.biUnion_𝓙, Set.subset_iUnion_of_subset, le_refl
40 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma TileStructure.Forest.union_𝓙₅ Part of Lemma 7.5.1 line 129 source
Source documentation
Part of Lemma 7.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, TileStructure.Forest, 𝔓, Membership.mem, Ne, LE.le and 5 more
Proof uses: Set.Subset.antisymm, Exists, Eq.mp, Eq.trans, congrArg, funext, TileStructure.Forest.𝓙, TileStructure.Forest.𝔖₀, Set.Iic, Set.mem_of_mem_of_subset, And.left, Prod.fst, GridStructure.Grid, Prod.mk, GridStructure.s, Prod.snd, TileStructure.Forest.𝓘_subset_iUnion_𝓙_𝔖₀, And, Eq.mpr, id and 55 more
93 instances, coercions and auxiliary constants left out.

Tactic trace: 44 steps
Open to load the checked before-and-after goal states.
```
lemma union_𝓙₅ (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (hu : u₁ ≠ u₂) (h2u : 𝓘 u₁ ≤ 𝓘 u₂) :
    ⋃ J ∈ 𝓙₅ t u₁ u₂, (J : Set X) = 𝓘 u₁ := by
…
```
Mentions: 𝓘, TileStructure.Forest.𝓙₅
lemma TileStructure.Forest.pairwiseDisjoint_𝓙₅ Part of Lemma 7.5.1 line 181 source
Source documentation
Part of Lemma 7.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, TileStructure.Forest, 𝔓, Set.PairwiseDisjoint, Grid, TileStructure.Forest.𝓙₅
Proof uses: LE.le, Inter.inter, TileStructure.Forest.𝓙, TileStructure.Forest.𝔖₀, Set.Iic, 𝓘, Set.inter_subset_left, Set.PairwiseDisjoint.subset, TileStructure.Forest.pairwiseDisjoint_𝓙
52 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma pairwiseDisjoint_𝓙₅ : (𝓙₅ t u₁ u₂).PairwiseDisjoint (fun I ↦ (I : Set X)) := by
…
```
Mentions: TileStructure.Forest.𝓙₅
lemma TileStructure.Forest.four_lt_sum_χtilde line 186 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 9 more
Proof uses: Exists, Eq.mp, Set.iUnion, congrArg, propext, Set.mem_iUnion₂, Eq.symm, TileStructure.Forest.union_𝓙₅, Grid.mem_def, LT.lt.trans_le, TileStructure.Forest.four_lt_χtilde, Finset.single_le_sum, Finset, zero_le, Eq.mpr, id, Eq, Set.mem_toFinset
70 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma TileStructure.Forest.bigger_than_𝓙_is_not_in_𝓙₀ line 195 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, LE.le, LT.lt, s and 4 more
Proof uses: And.right, Lean.Omega.Int.le_lt_asymm, Eq.mp, And, forall_congr, implies_congr, Eq.refl, Eq.trans, And.left, Prod.fst, GridStructure.Grid, Prod.mk, GridStructure.s, Prod.snd, le_of_lt
53 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma TileStructure.Forest.moderate_scale_change Lemma 7.5.3 (stated somewhat differently) line 207 source
Source documentation
Lemma 7.5.3 (stated somewhat differently).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, TileStructure.Forest, 𝔓, Grid, Membership.mem, TileStructure.Forest.𝓙₅ and 10 more
Proof uses: Decidable.byContradiction, TileStructure.Forest.𝔖₀, 𝓘, HAdd.hAdd, Or.resolve_left, Eq, Neg.neg, And.left, TileStructure.Forest.𝓙₀, TileStructure.Forest.𝓙, Set.Iic, Not.intro, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, LT.lt, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Nat.rawCast, Mathlib.Meta.NormNum.instAddMonoidWithOne and 125 more
247 instances, coercions and auxiliary constants left out.

Tactic trace: 38 steps
Open to load the checked before-and-after goal states.
```
lemma moderate_scale_change (hJ : J ∈ 𝓙₅ t u₁ u₂) (hJ' : J' ∈ 𝓙₅ t u₁ u₂)
    (hd : ¬Disjoint (ball (c J) (8 * D ^ s J)) (ball (c J') (8 * D ^ s J'))) :
    s J - 1 ≤ s J' := by
…
```
Mentions: TileStructure.Forest.𝓙₅, c, s
lemma TileStructure.Forest.sum_χ Part of Lemma 7.5.2 line 239 source
Source documentation
Part of Lemma 7.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, TileStructure.Forest, 𝔓, Membership.mem, Ne, LE.le and 10 more
Proof uses: id, Eq.mpr, HDiv.hDiv, TileStructure.Forest.χtilde, congrFun', congrArg, ite, LT.lt, NNReal.div_self_eq_ite, Classical.decPred, ite_congr, Eq.refl, Not, if_congr, Iff, Exists, And, Finset, funext, Metric.ball and 32 more
121 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
```
lemma sum_χ (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (hu : u₁ ≠ u₂) (h2u : 𝓘 u₁ ≤ 𝓘 u₂) (x : X) :
    ∑ J ∈ 𝓙₅ t u₁ u₂, χ t u₁ u₂ J x = (𝓘 u₁ : Set X).indicator 1 x := by
…
```
Mentions: 𝓘, TileStructure.Forest.𝓙₅, TileStructure.Forest.χ
lemma TileStructure.Forest.χ_le_indicator Part of Lemma 7.5.2 line 251 source
Source documentation
Part of Lemma 7.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, TileStructure.Forest, 𝔓, Grid, Membership.mem, TileStructure.Forest.𝓙₅ and 9 more
Proof uses: id, HDiv.hDiv, TileStructure.Forest.χtilde, Finset.sum, Set.toFinset, Classical.propDecidable, Eq.mpr, ite, Classical.decPred, Eq, congrArg, ite_congr, Eq.refl, Not, dite, ite_eq_left, NNReal.div_le_of_le_mul, one_mul, Finset.single_le_sum, Finset and 20 more
104 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
```
lemma χ_le_indicator (hJ : J ∈ 𝓙₅ t u₁ u₂) :
    χ t u₁ u₂ J x ≤ (ball (c J) (8 * D ^ s J)).indicator 1 x := by
…
```
Mentions: TileStructure.Forest.𝓙₅, TileStructure.Forest.χ, c, s
lemma TileStructure.Forest.χ_eq_zero_of_notMem_ball line 263 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, TileStructure.Forest, 𝔓, Grid, Membership.mem, TileStructure.Forest.𝓙₅ and 9 more
Proof uses: LE.le, Set.indicator, TileStructure.Forest.χ_le_indicator, Eq.mp, congrArg, propext, le_zero_iff, Set.indicator_of_notMem
65 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma TileStructure.Forest.boundedCompactSupport_toReal_χ line 268 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, TileStructure.Forest, 𝔓, Grid, Membership.mem, TileStructure.Forest.𝓙₅ and 3 more
Proof uses: MeasureTheory.BoundedCompactSupport.mono_norm, Set.indicator, Metric.ball, c, HMul.hMul, OfNat.ofNat, HPow.hPow, s, MeasureTheory.BoundedCompactSupport.mk, MeasureTheory.memLp_top_of_bound, MeasureTheory.AEStronglyMeasurable.indicator₀, MeasureTheory.aestronglyMeasurable_one, Eq.mpr, MeasureTheory.NullMeasurableSet, 𝕔, id, Eq, congrFun', MeasureTheory.Measure, congrArg and 41 more
123 instances, coercions and auxiliary constants left out.

Tactic trace: 23 steps
Open to load the checked before-and-after goal states.
lemma TileStructure.Forest.one_le_C7_5_2 line 287 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, NNReal, OfNat.ofNat, TileStructure.Forest.C7_5_2
Proof uses: Eq.mpr, HPow.hPow, HMul.hMul, HAdd.hAdd, 𝕔, HDiv.hDiv, id, Eq, congrArg, TileStructure.Forest.C7_5_2_def, cast, Eq.symm, Eq.trans, congrFun', Nat.cast_one, Nat.one_le_two_pow
38 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma TileStructure.Forest.quarter_add_two_mul_D_mul_card_le line 291 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, TileStructure.Forest, 𝔓, Grid, Membership.mem, TileStructure.Forest.𝓙₅ and 16 more
Proof uses: Finset, Eq.mpr, id, Eq, congrArg, rfl, 𝕔, ENNReal, MeasureTheory.Measure, MeasureTheory.MeasureSpace.volume, HSub.hSub, TileStructure.Forest.moderate_scale_change, And.left, Eq.mp, And, congrFun', And.right, propext, disjoint_comm, Trans.trans and 207 more
354 instances, coercions and auxiliary constants left out.

Tactic trace: 108 steps
Open to load the checked before-and-after goal states.
lemma TileStructure.Forest.dist_χ_le Part of Lemma 7.5.2 line 386 source
Source documentation
Part of Lemma 7.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, TileStructure.Forest, 𝔓, Grid, Membership.mem, Ne and 10 more
Proof uses: dite, And, Not, Metric.ball, c, OfNat.ofNat, Classical.propDecidable, Set.indicator, TileStructure.Forest.χ_le_indicator, Eq.mpr, id, Eq, congrArg, Eq.mp, propext, nonpos_iff_eq_zero, Set.indicator_of_notMem, And.left, And.right, dist_self and 192 more
300 instances, coercions and auxiliary constants left out.

Tactic trace: 94 steps
Open to load the checked before-and-after goal states.
```
lemma dist_χ_le (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (hu : u₁ ≠ u₂)
    (h2u : 𝓘 u₁ ≤ 𝓘 u₂) (hJ : J ∈ 𝓙₅ t u₁ u₂) (mx : x ∈ 𝓘 u₁) (mx' : x' ∈ 𝓘 u₁) :
    dist (χ t u₁ u₂ J x) (χ t u₁ u₂ J x') ≤ C7_5_2 a * dist x x' / D ^ s J := by
…
```
Mentions: 𝓘, TileStructure.Forest.𝓙₅, TileStructure.Forest.χ, s
lemma TileStructure.Forest.ψ_le_max line 484 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, LE.le, ψ, defaultD, Max.max, OfNat.ofNat, HPow.hPow, HSub.hSub, HMul.hMul, Inv.inv
Proof uses: dite, HDiv.hDiv, LE.le.trans, ψ_le_one, Real.one_le_rpow, le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HAdd.hAdd, inferInstance, AddMonoidWithOne, Mathlib.Meta.NormNum.instAtLeastTwo, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Int.rawCast, Ring, Int.negOfNat, Nat.rawCast and 80 more
116 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_of_mem_E line 496 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, E, Not, Metric.ball and 10 more
Proof uses: one_le_realD, Trans.trans, Eq, HAdd.hAdd, Eq.mpr, id, congrArg, mul_assoc, sub_le_sub_left, mul_le_mul_of_nonneg_left, propext, sub_le_iff_le_add, dist_triangle_left, le_of_lt, zpow_pos, lt_of_lt_of_le, Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_one, Eq.refl and 83 more
186 instances, coercions and auxiliary constants left out.

Tactic trace: 25 steps
Open to load the checked before-and-after goal states.
lemma TileStructure.Forest.enorm_ψ_le_edist line 515 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, E, Not, Metric.ball and 14 more
Proof uses: dite, Eq.mpr, id, Eq, congrArg, ψ_formula₄, enorm_zero, zero_le, HSub.hSub, le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HAdd.hAdd, inferInstance, AddMonoidWithOne, Mathlib.Meta.NormNum.instAtLeastTwo, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Int.rawCast and 120 more
264 instances, coercions and auxiliary constants left out.

Tactic trace: 30 steps
Open to load the checked before-and-after goal states.
lemma TileStructure.Forest.holder_correlation_tile_one line 538 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, 𝔓, MeasureTheory.BoundedCompactSupport, MeasureTheory.MeasureSpace.volume, Not, Membership.mem and 18 more
Proof uses: Trans.trans, C2_1_3, Eq, ψ, Neg.neg, Dist.dist, Ks, RingHom, starRingEnd, Complex.exp, Complex.I, HSub.hSub, FunctionDistances.Θ, MeasureTheory.SimpleFunc, Eq.mpr, id, congrArg, funext, Eq.trans, congrFun' and 126 more
303 instances, coercions and auxiliary constants left out.

Tactic trace: 34 steps
Open to load the checked before-and-after goal states.
lemma TileStructure.Forest.integrable_adjointCarleson_interior line 577 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, 𝔓, MeasureTheory.BoundedCompactSupport, MeasureTheory.MeasureSpace.volume, MeasureTheory.Integrable, HMul.hMul and 12 more
Proof uses: Filter.Eventually, LE.le, Norm.norm, ENNReal.toReal, MeasureTheory.eLpNorm, Top.top, ENNReal, MeasureTheory.ae, MeasureTheory.Measure, MeasureTheory.MemLp.ae_norm_le, MeasureTheory.BoundedCompactSupport.memLp_top, MeasureTheory.Integrable.const_mul, Eq.mpr, id, Eq, congrFun', congrArg, autoParam, funext, mul_rotate and 66 more
192 instances, coercions and auxiliary constants left out.

Tactic trace: 31 steps
Open to load the checked before-and-after goal states.
lemma TileStructure.Forest.holder_correlation_rearrange Sub-equations (7.5.10) and (7.5.11) in Lemma 7.5.5 line 607 source
Source documentation
Sub-equations (7.5.10) and (7.5.11) in Lemma 7.5.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, 𝔓, MeasureTheory.BoundedCompactSupport, MeasureTheory.MeasureSpace.volume, LE.le, ENNReal and 17 more
Proof uses: Trans.trans, Eq, RingHom, starRingEnd, OfNat.ofNat, MeasureTheory.integral, Eq.mpr, id, congrArg, edist_eq_enorm_sub, adjointCarleson.eq_1, Eq.symm, MeasureTheory.integral_const_mul, MeasureTheory.integral_sub, TileStructure.Forest.integrable_adjointCarleson_interior, Eq.refl, eq_of_heq, ENorm, HEq, HEq.refl and 94 more
270 instances, coercions and auxiliary constants left out.

Tactic trace: 37 steps
Open to load the checked before-and-after goal states.
```
lemma holder_correlation_rearrange (hf : BoundedCompactSupport f) :
    edist (exp (.I * 𝒬 u x) * adjointCarleson p f x) (exp (.I * 𝒬 u x') * adjointCarleson p f x') ≤
    (∫⁻ y in E p, ‖f y‖ₑ * ‖Ks (𝔰 p) y x‖ₑ * ‖- Q y x + Q y x' + 𝒬 u x - 𝒬 u x'‖ₑ) +
      ∫⁻ y in E p, ‖f y‖ₑ * ‖Ks (𝔰 p) y x - Ks (𝔰 p) y x'‖ₑ :=
…
```
Mentions: adjointCarleson, E, Ks, 𝔰
lemma TileStructure.Forest.QQQQ_bound_real line 670 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, E, TileStructure.Forest.𝔗 and 18 more
Proof uses: Eq, Ne, Or, eq_or_ne, Eq.mpr, Not, id, congrArg, ne_eq, propext, inv_eq_zero, Nat.cast_eq_zero, Not.intro, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, LT.lt, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Int.rawCast, inferInstance and 220 more
309 instances, coercions and auxiliary constants left out.

Tactic trace: 104 steps
Open to load the checked before-and-after goal states.
lemma TileStructure.Forest.QQQQ_bound line 751 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, E, TileStructure.Forest.𝔗 and 19 more
Proof uses: Trans.trans, Eq, Dist.dist, Eq.mpr, Norm.norm, id, congrArg, Eq.symm, enorm_norm, Real.enorm_le_enorm, norm_nonneg, TileStructure.Forest.QQQQ_bound_real, enorm_mul, Real.enorm_rpow_of_nonneg, div_nonneg, dist_nonneg, zpow_nonneg, Nat.cast_nonneg', Eq.trans, congrFun' and 37 more
224 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
lemma TileStructure.Forest.holder_correlation_tile_two line 767 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.𝔗, MeasureTheory.BoundedCompactSupport and 23 more
Proof uses: Trans.trans, HAdd.hAdd, C2_1_3, TileStructure.Forest.Q7_5_5, D2_1_3, Eq, Ks, HSub.hSub, Neg.neg, MeasureTheory.SimpleFunc, TileStructure.Forest.holder_correlation_rearrange, add_le_add, MeasureTheory.setLIntegral_mono', measurableSet_E, mul_le_mul', mul_le_mul_right, enorm_Ks_le, TileStructure.Forest.QQQQ_bound, MeasureTheory.lintegral_mono, le_refl and 148 more
311 instances, coercions and auxiliary constants left out.

Tactic trace: 67 steps
Open to load the checked before-and-after goal states.
lemma TileStructure.Forest.holder_correlation_tile Lemma 7.5.5 line 840 source
Source documentation
Lemma 7.5.5.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, TileStructure.Forest, 𝔓, Membership.mem, TileStructure.Forest.𝔗, MeasureTheory.BoundedCompactSupport and 23 more
Proof uses: dite, And, Not, Classical.propDecidable, Eq.mpr, Set.indicator, 𝓘, id, Eq, congrArg, TileStructure.Forest.adjoint_tile_support1, Set.indicator_of_notMem, And.left, And.right, of_eq_true, Eq.trans, 𝕔, True, congr, MulZeroClass.mul_zero and 23 more
191 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
```
lemma holder_correlation_tile (hu : u ∈ t) (hp : p ∈ t u) (hf : BoundedCompactSupport f) :
    edist (exp (.I * 𝒬 u x) * adjointCarleson p f x) (exp (.I * 𝒬 u x') * adjointCarleson p f x') ≤
    C7_5_5 a / volume (ball (𝔠 p) (4 * D ^ 𝔰 p)) *
      (edist x x' / D ^ 𝔰 p) ^ (a : ℝ)⁻¹ * ∫⁻ x in E p, ‖f x‖ₑ := by
…
```
Mentions: adjointCarleson, 𝔠, 𝔰, E
lemma TileStructure.Forest.limited_scale_impact_first_estimate Part of Lemma 7.5.6 line 859 source
Source documentation
Part of Lemma 7.5.6.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, TileStructure.Forest, 𝔓, Grid, Membership.mem, Ne and 17 more
Proof uses: Decidable.byContradiction, Iff.mpr, LT.lt, Int.not_le, Eq.mp, Iff.mp, HSub.hSub, Int.sub_one_lt_iff, Int.sub_lt_of_sub_lt, Eq.mpr, id, Eq, Eq.trans, Rat, congr, congrArg, Int.cast_sub, Int.cast_one, Rat.cast_sub, Rat.cast_intCast and 141 more
216 instances, coercions and auxiliary constants left out.

Tactic trace: 48 steps
Open to load the checked before-and-after goal states.
```
lemma limited_scale_impact_first_estimate (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (hu : u₁ ≠ u₂)
    (h2u : 𝓘 u₁ ≤ 𝓘 u₂) (hp : p ∈ t u₂ \ 𝔖₀ t u₁ u₂) (hJ : J ∈ 𝓙₅ t u₁ u₂)
    (h : ¬Disjoint (ball (𝔠 p) (8 * D ^ 𝔰 p)) (ball (c J) (8⁻¹ * D ^ s J))) : s J ≤ 𝔰 p := by
…
```
Mentions: 𝓘, TileStructure.Forest.𝔖₀, TileStructure.Forest.𝓙₅, 𝔠, 𝔰, c, s
lemma TileStructure.Forest.limited_scale_impact_second_estimate Part of Lemma 7.5.6 line 911 source
Source documentation
Part of Lemma 7.5.6.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, TileStructure.Forest, 𝔓, Grid, Membership.mem, SDiff.sdiff and 16 more
Proof uses: Decidable.byContradiction, Exists, And, Eq, False, Grid.exists_scale_succ, 𝓘, id, LT.lt, lt_of_not_ge, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, Neg.neg, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Nat.rawCast, Int.rawCast, inferInstance and 159 more
225 instances, coercions and auxiliary constants left out.

Tactic trace: 49 steps
Open to load the checked before-and-after goal states.
```
lemma limited_scale_impact_second_estimate (hp : p ∈ t u₂ \ 𝔖₀ t u₁ u₂) (hJ : J ∈ 𝓙₅ t u₁ u₂)
    (h : ¬Disjoint (ball (𝔠 p) (8 * D ^ 𝔰 p)) (ball (c J) (8⁻¹ * D ^ s J))) :
    𝔰 p ≤ s J + 3 := by
…
```
Mentions: TileStructure.Forest.𝔖₀, TileStructure.Forest.𝓙₅, 𝔠, 𝔰, c, s
lemma TileStructure.Forest.limited_scale_impact Lemma 7.5.6 line 975 source
Source documentation
Lemma 7.5.6.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, TileStructure.Forest, 𝔓, Grid, Membership.mem, Ne and 19 more
Proof uses: And.intro, TileStructure.Forest.limited_scale_impact_first_estimate, TileStructure.Forest.limited_scale_impact_second_estimate
98 instances, coercions and auxiliary constants left out.
```
lemma limited_scale_impact (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (hu : u₁ ≠ u₂)
    (h2u : 𝓘 u₁ ≤ 𝓘 u₂) (hp : p ∈ t u₂ \ 𝔖₀ t u₁ u₂) (hJ : J ∈ 𝓙₅ t u₁ u₂)
    (h : ¬ Disjoint (ball (𝔠 p) (8 * D ^ 𝔰 p)) (ball (c J) (8⁻¹ * D ^ s J))) :
    𝔰 p ∈ Icc (s J) (s J + 3) :=
…
```
Mentions: 𝓘, TileStructure.Forest.𝔖₀, TileStructure.Forest.𝓙₅, 𝔠, 𝔰, c, s
lemma TileStructure.Forest.local_tree_control_sumsumsup line 983 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, TileStructure.Forest, 𝔓, Grid, Membership.mem, Ne and 30 more
Proof uses: Trans.trans, Set.toFinset, Set.indicator, iSup₂_mono, id, Eq.mpr, NNNorm.nnnorm, congrArg, Finset.sum_congr, Eq.refl, Finset, congrFun', Set.filter_mem_univ_eq_toFinset, nnnorm_sum_le, eq_of_heq, SupSet, HEq, HEq.refl, Eq.symm, funext and 40 more
218 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
lemma TileStructure.Forest.local_tree_control_sup_bound line 1024 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, Membership.mem, Finset, Finset.Icc and 26 more
Proof uses: Trans.trans, MeasureTheory.integral, RingHom, starRingEnd, Ks, Complex.exp, Complex.I, HSub.hSub, FunctionDistances.Θ, MeasureTheory.SimpleFunc, HDiv.hDiv, C2_1_3, iSup₂_mono, MeasureTheory.enorm_integral_le_lintegral_enorm, eq_of_heq, SupSet, HEq, Eq.refl, HEq.refl, Eq.symm and 181 more
383 instances, coercions and auxiliary constants left out.

Tactic trace: 47 steps
Open to load the checked before-and-after goal states.
lemma TileStructure.Forest.local_tree_control Lemma 7.5.7 line 1080 source
Source documentation
Lemma 7.5.7.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, TileStructure.Forest, 𝔓, Grid, Membership.mem, Ne and 26 more
Proof uses: Trans.trans, HAdd.hAdd, 𝕔, Eq, Finset.sum, Finset.Icc, MeasureTheory.laverage, MeasureTheory.Measure.restrict, MeasureTheory.Measure, MeasureTheory.lintegral, Set.iUnion, Finset, Finset.filter, And, 𝔰, Not, Disjoint, 𝔠, Classical.propDecidable, Finset.univ and 204 more
353 instances, coercions and auxiliary constants left out.

Tactic trace: 68 steps
Open to load the checked before-and-after goal states.
```
lemma local_tree_control (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (hu : u₁ ≠ u₂)
    (h2u : 𝓘 u₁ ≤ 𝓘 u₂) (hJ : J ∈ 𝓙₅ t u₁ u₂) (hf : BoundedCompactSupport f) :
    ⨆ x ∈ ball (c J) (8⁻¹ * D ^ s J), ‖adjointCarlesonSum (t u₂ \ 𝔖₀ t u₁ u₂) f x‖ₑ ≤
    C7_5_7 a * ⨅ x ∈ J, maximalFunction volume 𝓑 c𝓑 r𝓑 1 f x := by
…
```
Mentions: 𝓘, TileStructure.Forest.𝓙₅, c, s, adjointCarlesonSum, TileStructure.Forest.𝔖₀, TileStructure.Forest.𝓑, TileStructure.Forest.c𝓑, TileStructure.Forest.r𝓑
lemma TileStructure.Forest.scales_impacting_interval Lemma 7.5.8 line 1152 source
Source documentation
Lemma 7.5.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, TileStructure.Forest, 𝔓, Grid, Membership.mem, Ne and 17 more
Proof uses: TileStructure.Forest.𝓙, Set.Iic, Or, Eq, Eq.mp, congrArg, propext, Set.mem_union, Or.inl, TileStructure.Forest.𝔗_subset_𝔖₀, Or.inr, And.right, Eq.refl, Neg.neg, HAdd.hAdd, TileStructure.Forest.𝓙₀, TileStructure.Forest.𝓙_subset_𝓙₀, Eq.rec, And.left, scale_mem_Icc and 45 more
177 instances, coercions and auxiliary constants left out.

Tactic trace: 30 steps
Open to load the checked before-and-after goal states.
```
lemma scales_impacting_interval (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (hu : u₁ ≠ u₂)
    (h2u : 𝓘 u₁ ≤ 𝓘 u₂) (hJ : J ∈ 𝓙₅ t u₁ u₂) (hp : p ∈ t u₁ ∪ (t u₂ ∩ 𝔖₀ t u₁ u₂))
    (h : ¬Disjoint (ball (𝔠 p) (8 * D ^ 𝔰 p)) (ball (c J) (16 * D ^ s J))) : s J ≤ 𝔰 p := by
…
```
Mentions: 𝓘, TileStructure.Forest.𝓙₅, TileStructure.Forest.𝔖₀, 𝔠, 𝔰, c, s
lemma TileStructure.Forest.volume_cpDsp_bound line 1183 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, Not, Disjoint, Metric.ball and 12 more
Proof uses: ENNReal.div_le_of_le_mul', HAdd.hAdd, Dist.dist, Trans.trans, add_le_add, LT.lt.le, MeasureTheory.dist_lt_of_not_disjoint_ball, le_refl, mul_le_mul_of_nonneg_left, zpow_le_zpow_right₀, one_le_realD, le_of_lt, Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Bool, Nat.ble, Eq.mpr, id and 39 more
172 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
lemma TileStructure.Forest.gtc_integral_bound line 1199 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, 𝔓, Membership.mem, Not, Disjoint and 21 more
Proof uses: Finset, Eq.mpr, id, congrArg, rfl, Trans.trans, Set.iUnion, Eq.symm, MeasureTheory.lintegral_biUnion_finset, Ne, Mathlib.Tactic.Contrapose.contrapose₂, Function.onFun, Exists, Iff.mp, Set.not_disjoint_iff, Eq.rec, And.right, Eq.mp, congrFun', 𝓘 and 51 more
186 instances, coercions and auxiliary constants left out.

Tactic trace: 26 steps
Open to load the checked before-and-after goal states.
lemma TileStructure.Forest.global_tree_control1_edist_part1 Part 1 of equation (7.5.18) of Lemma 7.5.9 line 1230 source
Source documentation
Part 1 of equation (7.5.18) of Lemma 7.5.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, TileStructure.Forest, 𝔓, Grid, Membership.mem, LE.le and 29 more
Proof uses: Trans.trans, Eq, MeasureTheory.Measure, MeasureTheory.lintegral, Finset.filter, And, Classical.propDecidable, Set.toFinset, E, adjointCarleson, id, Eq.mpr, Finset.univ, congrFun', congrArg, congr, Finset.mul_sum, Finset, Finset.ext, of_eq_true and 79 more
312 instances, coercions and auxiliary constants left out.

Tactic trace: 53 steps
Open to load the checked before-and-after goal states.
```
lemma global_tree_control1_edist_part1
    (hu : u ∈ t) {ℭ : Set (𝔓 X)} (hℭ : ℭ ⊆ t u) (hf : BoundedCompactSupport f)
    (hs : ∀ p ∈ ℭ, ¬Disjoint (ball (𝔠 p) (8 * D ^ 𝔰 p)) (ball (c J) (16 * D ^ s J)) → s J ≤ 𝔰 p)
    (hx : x ∈ ball (c J) (16 * D ^ s J)) (hx' : x' ∈ ball (c J) (16 * D ^ s J)) :
    edist (exp (.I * 𝒬 u x) * adjointCarlesonSum ℭ f x)
      (exp (.I * 𝒬 u x') * adjointCarlesonSum ℭ f x') ≤
    C7_5_5 a * 2 ^ (4 * a) * edist x x' ^ (a : ℝ)⁻¹ * ∑ k ∈ Finset.Icc (s J) S,
        D ^ (-k / (a : ℝ)) * ⨍⁻ x in ball (c J) (32 * D ^ k), ‖f x‖ₑ ∂volume := by
…
```
Mentions: ℭ, 𝔓, 𝔠, 𝔰, c, s, adjointCarlesonSum, k
lemma TileStructure.Forest.gtc_sum_Icc_le_two line 1303 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, LE.le, ENNReal, Finset.sum, Finset.Icc and 5 more
Proof uses: Trans.trans, Eq, tsum, Neg.neg, SummationFilter.unconditional, Int.toNat, Inv.inv, AddCommMonoid, Finset, Eq.rec, Eq.refl, funext, Eq.mpr, id, congrArg, Eq.symm, ENNReal.rpow_intCast, HMul.hMul, ENNReal.rpow_mul, HPow and 100 more
240 instances, coercions and auxiliary constants left out.

Tactic trace: 26 steps
Open to load the checked before-and-after goal states.
lemma TileStructure.Forest.global_tree_control1_edist_part2 Part 2 of equation (7.5.18) of Lemma 7.5.9 line 1331 source
Source documentation
Part 2 of equation (7.5.18) of Lemma 7.5.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, TileStructure.Forest, 𝔓, Grid, Membership.mem, LE.le and 29 more
Proof uses: Trans.trans, Eq, TileStructure.Forest.C7_5_5, HAdd.hAdd, Finset.sum, Finset.Icc, HSub.hSub, Neg.neg, MeasureTheory.laverage, MeasureTheory.Measure.restrict, ENorm.enorm, TileStructure.Forest.global_tree_control1_edist_part1, mul_le_mul', le_refl, Finset.sum_le_sum, Finset, TileStructure.Forest.laverage_le_biInf_MB, mul_le_mul, Mathlib.Meta.NormNum.isNat_le_true, Mathlib.Meta.NormNum.isNat_ofNat and 102 more
376 instances, coercions and auxiliary constants left out.

Tactic trace: 41 steps
Open to load the checked before-and-after goal states.
```
lemma global_tree_control1_edist_part2
    (hu : u ∈ t) {ℭ : Set (𝔓 X)} (hℭ : ℭ ⊆ t u) (hf : BoundedCompactSupport f)
    (hs : ∀ p ∈ ℭ, ¬Disjoint (ball (𝔠 p) (8 * D ^ 𝔰 p)) (ball (c J) (16 * D ^ s J)) → s J ≤ 𝔰 p)
    (hx : x ∈ ball (c J) (16 * D ^ s J)) (hx' : x' ∈ ball (c J) (16 * D ^ s J)) :
    edist (exp (.I * 𝒬 u x) * adjointCarlesonSum ℭ f x)
      (exp (.I * 𝒬 u x') * adjointCarlesonSum ℭ f x') ≤
    C7_5_9d a * (edist x x' / D ^ s J) ^ (a : ℝ)⁻¹ * ⨅ x ∈ J, maximalFunction volume 𝓑 c𝓑 r𝓑 1 f x := by
…
```
Mentions: ℭ, 𝔓, 𝔠, 𝔰, c, s, adjointCarlesonSum, TileStructure.Forest.𝓑, TileStructure.Forest.c𝓑, TileStructure.Forest.r𝓑
lemma TileStructure.Forest.global_tree_control1_edist_left Equation (7.5.18) of Lemma 7.5.9 for ℭ = t u₁ line 1377 source
Source documentation
Equation (7.5.18) of Lemma 7.5.9 for ℭ = t u₁.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, TileStructure.Forest, 𝔓, Grid, Membership.mem, Ne and 28 more
Proof uses: TileStructure.Forest.global_tree_control1_edist_part2, subset_rfl, Not, Disjoint, 𝔠, 𝔰, TileStructure.Forest.scales_impacting_interval, Set.mem_union_left, Inter.inter, TileStructure.Forest.𝔖₀
140 instances, coercions and auxiliary constants left out.
```
lemma global_tree_control1_edist_left (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (hu : u₁ ≠ u₂)
    (h2u : 𝓘 u₁ ≤ 𝓘 u₂) (hJ : J ∈ 𝓙₅ t u₁ u₂) (hf : BoundedCompactSupport f)
    (hx : x ∈ ball (c J) (16 * D ^ s J)) (hx' : x' ∈ ball (c J) (16 * D ^ s J)) :
    edist (exp (.I * 𝒬 u₁ x) * adjointCarlesonSum (t u₁) f x)
      (exp (.I * 𝒬 u₁ x') * adjointCarlesonSum (t u₁) f x') ≤
    C7_5_9d a * (edist x x' / D ^ s J) ^ (a : ℝ)⁻¹ * ⨅ x ∈ J, maximalFunction volume 𝓑 c𝓑 r𝓑 1 f x :=
…
```
Mentions: 𝓘, TileStructure.Forest.𝓙₅, c, s, adjointCarlesonSum, TileStructure.Forest.𝓑, TileStructure.Forest.c𝓑, TileStructure.Forest.r𝓑
lemma TileStructure.Forest.global_tree_control1_edist_right Equation (7.5.18) of Lemma 7.5.9 for ℭ = t u₂ ∩ 𝔖₀ t u₁ u₂ line 1387 source
Source documentation
Equation (7.5.18) of Lemma 7.5.9 for ℭ = t u₂ ∩ 𝔖₀ t u₁ u₂.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, TileStructure.Forest, 𝔓, Grid, Membership.mem, Ne and 30 more
Proof uses: TileStructure.Forest.global_tree_control1_edist_part2, Set.inter_subset_left, Not, Disjoint, 𝔠, 𝔰, TileStructure.Forest.scales_impacting_interval, Set.mem_union_right
140 instances, coercions and auxiliary constants left out.
```
lemma global_tree_control1_edist_right (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (hu : u₁ ≠ u₂)
    (h2u : 𝓘 u₁ ≤ 𝓘 u₂) (hJ : J ∈ 𝓙₅ t u₁ u₂) (hf : BoundedCompactSupport f)
    (hx : x ∈ ball (c J) (16 * D ^ s J)) (hx' : x' ∈ ball (c J) (16 * D ^ s J)) :
    edist (exp (.I * 𝒬 u₂ x) * adjointCarlesonSum (t u₂ ∩ 𝔖₀ t u₁ u₂) f x)
      (exp (.I * 𝒬 u₂ x') * adjointCarlesonSum (t u₂ ∩ 𝔖₀ t u₁ u₂) f x') ≤
    C7_5_9d a * (edist x x' / D ^ s J) ^ (a : ℝ)⁻¹ * ⨅ x ∈ J, maximalFunction volume 𝓑 c𝓑 r𝓑 1 f x :=
…
```
Mentions: 𝓘, TileStructure.Forest.𝓙₅, c, s, adjointCarlesonSum, TileStructure.Forest.𝔖₀, TileStructure.Forest.𝓑, TileStructure.Forest.c𝓑, TileStructure.Forest.r𝓑
lemma TileStructure.Forest.one_le_C7_5_9s line 1400 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, NNReal, OfNat.ofNat, TileStructure.Forest.C7_5_9s
Proof uses: Eq.mpr, HMul.hMul, HPow.hPow, HAdd.hAdd, 𝕔, HDiv.hDiv, id, Eq, congrArg, Eq.trans, TileStructure.Forest.C7_5_5, TileStructure.Forest.C7_5_9s_def, congrFun', TileStructure.Forest.C7_5_5_def, Eq.symm, Nat.cast_one, congr, pow_add, Nat.one_le_two_pow
44 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma TileStructure.Forest.C7_5_9d_le_C7_5_9s line 1404 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, NNReal, TileStructure.Forest.C7_5_9d, TileStructure.Forest.C7_5_9s
Proof uses: Eq.mpr, HMul.hMul, TileStructure.Forest.C7_5_5, HPow.hPow, OfNat.ofNat, HAdd.hAdd, id, Eq, congr, congrArg, TileStructure.Forest.C7_5_9d_def, TileStructure.Forest.C7_5_9s_def, mul_le_mul_right, pow_le_pow_right', one_le_two, add_le_add_right, NeZero.one_le
34 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma TileStructure.Forest.global_tree_control1_supbound Equation (7.5.17) of Lemma 7.5.9 line 1409 source
Source documentation
Equation (7.5.17) of Lemma 7.5.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, TileStructure.Forest, 𝔓, Grid, Membership.mem, Ne and 29 more
Proof uses: Eq.mpr, HSub.hSub, id, congrArg, Eq.symm, propext, tsub_le_iff_left, ENNReal.le_of_forall_pos_le_add, LT.lt, Top.top, And, HDiv.hDiv, Exists, ENNReal.exists_biSup_le_enorm_add_eps, div_pos, Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Bool and 167 more
366 instances, coercions and auxiliary constants left out.

Tactic trace: 71 steps
Open to load the checked before-and-after goal states.
```
lemma global_tree_control1_supbound (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (hu : u₁ ≠ u₂)
    (h2u : 𝓘 u₁ ≤ 𝓘 u₂) (ℭ : Set (𝔓 X)) (hℭ : ℭ = t u₁ ∨ ℭ = t u₂ ∩ 𝔖₀ t u₁ u₂)
    (hJ : J ∈ 𝓙₅ t u₁ u₂) (hf : BoundedCompactSupport f) :
    ⨆ x ∈ ball (c J) (16 * D ^ s J), ‖adjointCarlesonSum ℭ f x‖ₑ ≤
    (⨅ x ∈ ball (c J) (8⁻¹ * D ^ s J), ‖adjointCarlesonSum ℭ f x‖ₑ) +
    C7_5_9s a * ⨅ x ∈ J, maximalFunction volume 𝓑 c𝓑 r𝓑 1 f x := by
…
```
Mentions: 𝓘, ℭ, 𝔓, TileStructure.Forest.𝔖₀, TileStructure.Forest.𝓙₅, c, s, adjointCarlesonSum, TileStructure.Forest.𝓑, TileStructure.Forest.c𝓑, TileStructure.Forest.r𝓑
lemma TileStructure.Forest.le_C7_5_10 line 1478 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, NNReal, HAdd.hAdd, TileStructure.Forest.C7_5_7, TileStructure.Forest.C7_5_9s, TileStructure.Forest.C7_5_10
Proof uses: Eq.mpr, HPow.hPow, HMul.hMul, 𝕔, HDiv.hDiv, id, Eq, congr, congrArg, TileStructure.Forest.C7_5_7_def, Eq.trans, TileStructure.Forest.C7_5_5, TileStructure.Forest.C7_5_9s_def, congrFun', TileStructure.Forest.C7_5_5_def, TileStructure.Forest.C7_5_10_def, add_le_pow_two, mul_le_mul', seven_le_c, le_refl and 79 more
103 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
lemma TileStructure.Forest.C7_5_9s_le_C7_5_10 line 1488 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, NNReal, TileStructure.Forest.C7_5_9s, TileStructure.Forest.C7_5_10
Proof uses: le_trans, HAdd.hAdd, TileStructure.Forest.C7_5_7, le_add_self, TileStructure.Forest.le_C7_5_10
15 instances, coercions and auxiliary constants left out.
lemma TileStructure.Forest.one_le_C7_5_10 line 1491 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, NNReal, TileStructure.Forest.C7_5_10
Proof uses: LE.le.trans, TileStructure.Forest.C7_5_9s, TileStructure.Forest.one_le_C7_5_9s, TileStructure.Forest.C7_5_9s_le_C7_5_10
13 instances, coercions and auxiliary constants left out.
lemma TileStructure.Forest.global_tree_control2 Lemma 7.5.10 line 1495 source
Source documentation
Lemma 7.5.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, TileStructure.Forest, 𝔓, Grid, Membership.mem, Ne and 27 more
Proof uses: Trans.trans, TileStructure.Forest.C7_5_7, TileStructure.Forest.C7_5_9s, SDiff.sdiff, HSub.hSub, Eq, TileStructure.Forest.global_tree_control1_supbound, Or.inr, rfl, eq_of_heq, outParam, HAdd, HEq, Eq.refl, HEq.refl, Eq.symm, InfSet, funext, iInf_congr_Prop, iff_of_eq and 14 more
165 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
lemma global_tree_control2 (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (hu : u₁ ≠ u₂)
    (h2u : 𝓘 u₁ ≤ 𝓘 u₂) (hJ : J ∈ 𝓙₅ t u₁ u₂) (hf : BoundedCompactSupport f) :
    ⨆ x ∈ ball (c J) (16 * D ^ s J), ‖adjointCarlesonSum (t u₂ ∩ 𝔖₀ t u₁ u₂) f x‖ₑ ≤
    (⨅ x ∈ ball (c J) (8⁻¹ * D ^ s J), ‖adjointCarlesonSum (t u₂) f x‖ₑ) +
    C7_5_10 a * ⨅ x ∈ J, maximalFunction volume 𝓑 c𝓑 r𝓑 1 f x :=
…
```
Mentions: 𝓘, TileStructure.Forest.𝓙₅, c, s, adjointCarlesonSum, TileStructure.Forest.𝔖₀, TileStructure.Forest.𝓑, TileStructure.Forest.c𝓑, TileStructure.Forest.r𝓑
def TileStructure.Forest.P7_5_4 The product on the right-hand side of Lemma 7.5.4 line 1521 source
Source documentation
The product on the right-hand side of Lemma 7.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, TileStructure.Forest, 𝔓, Grid, ENNReal
Proof uses: HMul.hMul, HAdd.hAdd, iInf, Membership.mem, Metric.ball, c, Inv.inv, OfNat.ofNat, HPow.hPow, s, ENorm.enorm, adjointCarlesonSum, TileStructure.Forest.𝔗, maximalFunction, Prod, MeasureTheory.MeasureSpace.volume, TileStructure.Forest.𝓑, TileStructure.Forest.c𝓑, TileStructure.Forest.r𝓑
69 instances, coercions and auxiliary constants left out.
```
def P7_5_4 (t : Forest X n) (u₁ u₂ : 𝔓 X) (f₁ f₂ : X → ℂ) (J : Grid X) : ℝ≥0∞ :=
…
```
Mentions: TileStructure.Forest, 𝔓, Grid
lemma TileStructure.Forest.P7_5_4_le_adjointBoundaryOperator_mul line 1527 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, TileStructure.Forest, 𝔓, Grid, Membership.mem, Metric.ball and 10 more
Proof uses: LE.le.trans, GridStructure.c, HDiv.hDiv, GridStructure.s, Metric.ball_subset_ball, id, Eq.mpr, Eq, congrArg, div_eq_inv_mul, mul_le_mul_of_nonneg_right, inv_anti₀, Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Bool, Nat.ble, Mathlib.Meta.NormNum.isNat_le_true, Bool.true and 22 more
166 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
lemma TileStructure.Forest.support_holderFunction_subset The support of holderFunction is in 𝓘 u₁ line 1540 source
Source documentation
The support of holderFunction is in 𝓘 u₁.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, TileStructure.Forest, 𝔓, Grid, Membership.mem, LE.le and 3 more
Proof uses: Eq.mpr, Not, Eq, OfNat.ofNat, id, congrArg, propext, Function.support_subset_iff', adjointCarlesonSum, TileStructure.Forest.𝔗, Finset.sum_eq_zero, Finset.filter, Classical.propDecidable, Finset.univ, adjointCarleson, Finset, Set.indicator, TileStructure.Forest.adjoint_tile_support2, Eq.mp, Set.indicator_of_notMem and 14 more
66 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
lemma support_holderFunction_subset (u₂ : 𝔓 X) (f₁ f₂ : X → ℂ) (J : Grid X) (hu₁ : u₁ ∈ t) :
    support (holderFunction t u₁ u₂ f₁ f₂ J) ⊆ 𝓘 u₁ := by
…
```
Mentions: 𝔓, Grid, TileStructure.Forest.holderFunction, 𝓘
lemma TileStructure.Forest.enorm_holderFunction_le line 1550 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, TileStructure.Forest, 𝔓, Grid, Membership.mem, Ne and 17 more
Proof uses: id, Eq.mpr, TileStructure.Forest.χ, Complex.exp, Complex.I, FunctionDistances.Θ, PreTileStructure.𝒬, adjointCarlesonSum, TileStructure.Forest.𝔗, RingHom, starRingEnd, Inter.inter, TileStructure.Forest.𝔖₀, Eq, congrFun', congrArg, Eq.trans, enorm_mul, RCLike.enorm_conj, congr and 38 more
169 instances, coercions and auxiliary constants left out.

Tactic trace: 27 steps
Open to load the checked before-and-after goal states.
lemma TileStructure.Forest.holder_correlation_tree_1 line 1578 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, TileStructure.Forest, 𝔓, Grid, Membership.mem, Ne and 28 more
Proof uses: id, Eq.mpr, Eq, congrFun', congrArg, congr, enorm_mul, Complex.enorm_exp_I_mul_ofReal, one_mul, dite, Not, Classical.propDecidable, Finset.sum_eq_zero, Finset.filter, Finset.univ, adjointCarleson, Finset, Set.indicator, TileStructure.Forest.adjoint_tile_support2, Eq.mp and 79 more
274 instances, coercions and auxiliary constants left out.

Tactic trace: 38 steps
Open to load the checked before-and-after goal states.
lemma TileStructure.Forest.holder_correlation_tree_2 line 1620 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, TileStructure.Forest, 𝔓, Grid, Membership.mem, Ne and 28 more
Proof uses: Trans.trans, Eq, HAdd.hAdd, iInf, maximalFunction, Prod, TileStructure.Forest.𝓑, TileStructure.Forest.c𝓑, TileStructure.Forest.r𝓑, mul_le_mul', Eq.mpr, id, congrArg, propext, ENNReal.coe_le_one_iff, LE.le.trans, Set.indicator, TileStructure.Forest.χ_le_indicator, Set.indicator_le, le_refl and 38 more
209 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
lemma TileStructure.Forest.holder_correlation_tree_3 line 1651 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, TileStructure.Forest, 𝔓, Grid, Membership.mem, Ne and 28 more
Proof uses: Trans.trans, Eq, HAdd.hAdd, iInf, maximalFunction, Prod, TileStructure.Forest.𝓑, TileStructure.Forest.c𝓑, TileStructure.Forest.r𝓑, mul_le_mul', Eq.mpr, id, congrArg, propext, ENNReal.coe_le_one_iff, LE.le.trans, Set.indicator, TileStructure.Forest.χ_le_indicator, Set.indicator_le, le_refl and 38 more
209 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
def TileStructure.Forest.I7_5_4 An intermediate constant in Lemma 7.5.4 line 1684 source
Source documentation
An intermediate constant in Lemma 7.5.4.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NNReal
Proof uses: HPow.hPow, OfNat.ofNat, HAdd.hAdd, HMul.hMul, 𝕔, HDiv.hDiv
19 instances, coercions and auxiliary constants left out.
```
def I7_5_4 (a : ℕ) : ℝ≥0 := 2 ^ ((4 * 𝕔 + 9 + 3 * (𝕔 / 4)) * a ^ 3 + 12 * a)
```
lemma TileStructure.Forest.le_I7_5_4 line 1686 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, NNReal, HAdd.hAdd, HMul.hMul, TileStructure.Forest.C7_5_2, TileStructure.Forest.C7_5_9s, TileStructure.Forest.C7_5_10, TileStructure.Forest.C7_5_9d, TileStructure.Forest.I7_5_4
Proof uses: Eq, HPow.hPow, Mathlib.Meta.NormNum.isNat_eq_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Mathlib.Meta.NormNum.isNat_pow, Mathlib.Meta.NormNum.IsNatPowT.run, Mathlib.Meta.NormNum.IsNatPowT.trans, Nat.pow, Mathlib.Meta.NormNum.IsNatPowT.bit0, Mathlib.Meta.NormNum.IsNatPowT.bit1, Eq.mpr, 𝕔, HDiv.hDiv, id, congrFun', congrArg, congr, Eq.trans and 86 more
108 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
lemma TileStructure.Forest.edist_holderFunction_le line 1700 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, TileStructure.Forest, 𝔓, Grid, Membership.mem, Ne and 18 more
Proof uses: dite, And, Not, Classical.propDecidable, Eq, Iff.mp, Function.support, Function.support_subset_iff', TileStructure.Forest.support_holderFunction_subset, Eq.mpr, id, congrArg, And.left, And.right, WeakPseudoEMetricSpace.edist_self, zero_le, Or, Classical.em, TileStructure.Forest.χ, Complex.exp and 109 more
288 instances, coercions and auxiliary constants left out.

Tactic trace: 51 steps
Open to load the checked before-and-after goal states.
lemma TileStructure.Forest.le_C7_5_4 line 1765 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, NNReal, HAdd.hAdd, HMul.hMul, TileStructure.Forest.C7_5_9s, TileStructure.Forest.C7_5_10, HPow.hPow, Real, defaultτ, TileStructure.Forest.I7_5_4, TileStructure.Forest.C7_5_4
Proof uses: Eq.mpr, Inv.inv, id, Eq, congrArg, defaultτ.eq_1, Mathlib.Meta.NormNum.isNat_eq_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Eq.rec, Mathlib.Meta.NormNum.IsNat, Mathlib.Meta.NormNum.isNat_pow, Mathlib.Meta.NormNum.IsNat.raw_refl, Mathlib.Meta.NormNum.IsNatPowT.run, Mathlib.Meta.NormNum.IsNatPowT.trans, Nat.pow, Mathlib.Meta.NormNum.IsNatPowT.bit0, Eq.symm, Mathlib.Meta.NormNum.IsNat.nnreal_rpow_eq_nnreal_pow and 105 more
163 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
lemma TileStructure.Forest.holder_correlation_tree Lemma 7.5.4 line 1785 source
Source documentation
Lemma 7.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, TileStructure.Forest, 𝔓, Grid, Membership.mem, Ne and 16 more
Proof uses: id, Trans.trans, HAdd.hAdd, iSup, Metric.ball, ENorm.enorm, ENNReal.ofReal, HDiv.hDiv, HSub.hSub, EDist.edist, TileStructure.Forest.C7_5_9s, TileStructure.Forest.C7_5_10, TileStructure.Forest.I7_5_4, Eq, Inv.inv, add_le_add, Iff.mpr, iSup₂_le_iff, TileStructure.Forest.enorm_holderFunction_le, mul_le_mul' and 67 more
242 instances, coercions and auxiliary constants left out.

Tactic trace: 34 steps
Open to load the checked before-and-after goal states.
```
lemma holder_correlation_tree (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (hu : u₁ ≠ u₂) (h2u : 𝓘 u₁ ≤ 𝓘 u₂)
    (hJ : J ∈ 𝓙₅ t u₁ u₂) (hf₁ : BoundedCompactSupport f₁) (hf₂ : BoundedCompactSupport f₂) :
    iHolENorm (holderFunction t u₁ u₂ f₁ f₂ J) (c J) (16 * D ^ s J) τ ≤
    C7_5_4 a * P7_5_4 t u₁ u₂ f₁ f₂ J := by
…
```
Mentions: 𝓘, TileStructure.Forest.𝓙₅, iHolENorm, TileStructure.Forest.holderFunction, c, s, TileStructure.Forest.P7_5_4
lemma TileStructure.Forest.C7_5_11_binomial_bound A binomial bound used in Lemma 7.4.5 line 1837 source
Source documentation
A binomial bound used in Lemma 7.4.5.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, ENNReal, HPow.hPow, Real, HAdd.hAdd, TileStructure.Forest.C7_5_11, Neg.neg, Inv.inv, HMul.hMul, HDiv.hDiv, 𝕔, defaultZ
Proof uses: Trans.trans, Eq, HSub.hSub, Eq.mpr, id, congrArg, ENNReal.rpow_mul, ENNReal.rpow_le_rpow_of_nonpos, propext, Left.neg_nonpos_iff, le_of_lt, inv_pos_of_pos, add_pos', mul_pos, Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Bool, Nat.ble and 117 more
252 instances, coercions and auxiliary constants left out.

Tactic trace: 37 steps
Open to load the checked before-and-after goal states.
```
lemma C7_5_11_binomial_bound (a4 : 4 ≤ a) :
    (1 + C7_5_11 a n : ℝ≥0∞) ^ (-(2 * a ^ 2 + a ^ 3 : ℝ)⁻¹) ≤
    2 ^ ((𝕔 / 4) * a ^ 3 + 7) * 2 ^ (-(Z * n : ℝ) / (4 * a ^ 2 + 2 * a ^ 3)) :=
…
```
lemma TileStructure.Forest.lower_oscillation_bound Lemma 7.5.11 line 1869 source
Source documentation
Lemma 7.5.11

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, TileStructure.Forest, 𝔓, Grid, Membership.mem, Ne and 12 more
Proof uses: Exists, And, Eq, HAdd.hAdd, Grid.exists_scale_succ, TileStructure.Forest.𝓙, TileStructure.Forest.𝔖₀, Set.Iic, LT.lt, TileStructure.Forest.𝓙₀, Prod.fst, GridStructure.Grid, Prod.mk, GridStructure.s, Prod.snd, TileStructure.Forest.𝔗, Set.Nonempty, TileStructure.Forest.nonempty', lt_of_le_of_ne, id and 145 more
205 instances, coercions and auxiliary constants left out.

Tactic trace: 64 steps
Open to load the checked before-and-after goal states.
```
lemma lower_oscillation_bound (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (hu : u₁ ≠ u₂)
    (h2u : 𝓘 u₁ ≤ 𝓘 u₂) (hJ : J ∈ 𝓙₅ t u₁ u₂) :
    C7_5_11 a n ≤ dist_{c J, 8 * D ^ s J} (𝒬 u₁) (𝒬 u₂) := by
…
```
Mentions: 𝓘, TileStructure.Forest.𝓙₅, c, s
lemma TileStructure.Forest.cdtp_le_iHolENorm line 1954 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 34 more
Proof uses: Eq, TileStructure.Forest.χ, Complex.exp, Complex.I, HSub.hSub, FunctionDistances.Θ, id, Eq.mpr, congrArg, map_mul, congr, Eq.trans, congrFun', HMul, Eq.rec, Eq.refl, Eq.symm, mul_rotate, Complex.exp_conj, Complex.conj_I and 62 more
278 instances, coercions and auxiliary constants left out.

Tactic trace: 28 steps
Open to load the checked before-and-after goal states.
lemma TileStructure.Forest.le_C7_4_5 line 2003 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, NNReal, HMul.hMul, C2_0_5, Real, TileStructure.Forest.C7_5_4, HPow.hPow, HAdd.hAdd, HDiv.hDiv, 𝕔, Neg.neg, defaultZ, TileStructure.Forest.C7_4_5
Proof uses: Eq.mpr, id, Eq, congrArg, C2_0_5.eq_1, TileStructure.Forest.C7_5_4_def, TileStructure.Forest.C7_4_5_def, Eq.rec, Eq.refl, Eq.trans, congrFun', NNReal.rpow_natCast, mul_le_mul', pow_le_pow_right₀, one_le_two, le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Int, Eq.mp and 72 more
144 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma TileStructure.Forest.correlation_distant_tree_parts Lemma 7.4.5 line 2014 source
Source documentation
Lemma 7.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, TileStructure.Forest, 𝔓, Membership.mem, Ne, LE.le and 19 more
Proof uses: Trans.trans, MeasureTheory.lintegral, Eq, MeasureTheory.Measure.restrict, Finset.sum, Set.toFinset, TileStructure.Forest.𝓙₅, Classical.propDecidable, Metric.ball, c, Inv.inv, HPow.hPow, s, C2_0_5, TileStructure.Forest.C7_5_4, HAdd.hAdd, HDiv.hDiv, 𝕔, Neg.neg, defaultZ and 157 more
289 instances, coercions and auxiliary constants left out.

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