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

29 declarations, 0 contain sorry, 0 declared as axioms

6.1. The density arguments

This file contains the proofs of lemmas 6.1.1, 6.1.2 and 6.1.3 from the blueprint.

Main results

tile_disjointness: Lemma 6.1.1.
maximal_bound_antichain: Lemma 6.1.2.
dens2_antichain: Lemma 6.1.3.

Imports (4)

Imported by 2 files

lemma inv_nnqt_eq line 38 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, Eq, Inv.inv, HDiv.hDiv, HMul.hMul, OfNat.ofNat, nnq, HAdd.hAdd
Proof uses: Ne, Not.intro, Mathlib.Tactic.Linarith.lt_irrefl, outParam, Eq.mp, LT.lt, Neg.neg, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Int.rawCast, inferInstance, Ring, Int.negOfNat, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.Common.neg_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat and 84 more
112 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma inv_nnqt_mem_Ico line 43 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, Membership.mem, Set.Ico, HDiv.hDiv, OfNat.ofNat, Inv.inv, HMul.hMul, nnq, HAdd.hAdd
Proof uses: Eq.mpr, id, Eq, congrArg, inv_nnqt_eq, And.intro, LE.le, LT.lt, le_of_not_gt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HSub.hSub, inferInstance, AddMonoidWithOne, Mathlib.Meta.NormNum.instAtLeastTwo, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Int.rawCast, Ring, Int.negOfNat and 77 more
107 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma one_lt_nnqt line 47 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, LT.lt, NNReal, OfNat.ofNat, HDiv.hDiv, HMul.hMul, nnq, HAdd.hAdd
Proof uses: Eq.mpr, id, Eq, congrArg, propext, one_lt_div, Iff.mpr, Or, add_pos_iff, Or.inr, zero_lt_one, two_mul, add_lt_add_iff_left, And.left, outParam, LE.le, ProofData.q_mem_Ioc
86 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma one_lt_nnqt_coe line 51 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, LT.lt, ENNReal, OfNat.ofNat, HDiv.hDiv, HMul.hMul, nnq, HAdd.hAdd
Proof uses: Eq.mpr, NNReal, id, Eq, congrArg, Eq.symm, ENNReal.coe_ofNat, ENNReal.coe_one, ENNReal.coe_add, ENNReal.coe_mul, ENNReal.coe_div, of_eq_true, Not, Eq.trans, False, True, And, AddUnits, and_false, not_false_eq_true and 3 more
72 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma nnqt_lt_nnq line 55 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, LT.lt, NNReal, HDiv.hDiv, HMul.hMul, OfNat.ofNat, nnq, HAdd.hAdd
Proof uses: Eq.mpr, id, Eq, congrArg, add_comm, propext, div_lt_iff₀, add_pos, zero_lt_one, nnq_pos, mul_comm, mul_lt_mul_iff_of_pos_left, Eq.symm, one_add_one_eq_two, add_lt_add_iff_left, And.left, LE.le, nnq_mem_Ioc
94 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma nnqt_lt_nnq_coe line 60 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, LT.lt, ENNReal, HDiv.hDiv, HMul.hMul, OfNat.ofNat, nnq, HAdd.hAdd
Proof uses: Eq.mpr, NNReal, id, Eq, congrArg, Eq.symm, ENNReal.coe_ofNat, ENNReal.coe_one, ENNReal.coe_add, ENNReal.coe_mul, ENNReal.coe_div, of_eq_true, Not, Eq.trans, False, True, And, AddUnits, and_false, not_false_eq_true and 3 more
72 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma nnqt_lt_two line 64 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, LT.lt, NNReal, HDiv.hDiv, HMul.hMul, OfNat.ofNat, nnq, HAdd.hAdd
Proof uses: lt_of_lt_of_le, nnqt_lt_nnq, And.right, LE.le, nnq_mem_Ioc
45 instances, coercions and auxiliary constants left out.
lemma nnqt_lt_two_coe line 66 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, LT.lt, ENNReal, HDiv.hDiv, HMul.hMul, OfNat.ofNat, nnq, HAdd.hAdd
Proof uses: Eq.mpr, NNReal, id, Eq, congrArg, Eq.symm, ENNReal.coe_ofNat, ENNReal.coe_one, ENNReal.coe_add, ENNReal.coe_mul, ENNReal.coe_div, of_eq_true, Not, Eq.trans, False, True, And, AddUnits, and_false, not_false_eq_true and 3 more
72 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma tile_disjointness Lemma 6.1.1 line 80 source
Source documentation
Lemma 6.1.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, 𝔓, IsAntichain, LE.le, Membership.mem, Not and 3 more
Proof uses: 𝔰, Or, Classical.em, And, Exists, Iff.mp, Set.not_disjoint_iff, Grid, 𝓘, FunctionDistances.Θ, TileStructure.Ω, MeasureTheory.SimpleFunc, Set.Icc, or_iff_left, Iff.mpr, Exists.intro, And.intro, le_or_disjoint, or_iff_right, TileStructure.relative_fundamental_dyadic and 14 more
85 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
```
lemma tile_disjointness {𝔄 : Set (𝔓 X)} (h𝔄 : IsAntichain (· ≤ ·) (𝔄 : Set (𝔓 X)))
     {p p' : 𝔓 X} (hp : p ∈ 𝔄) (hp' : p' ∈ 𝔄) (hE : ¬Disjoint (E p) (E p')) : p = p' := by
…
```
Mentions: 𝔓, E
def C6_1_2 Constant appearing in Lemma 6.1.2 line 97 source
Source documentation
Constant appearing in Lemma 6.1.2. Has value 2 ^ (102 * a ^ 3) in the blueprint.

standard axioms: propext what this means
Statement uses: Nat
Proof uses: HPow.hPow, OfNat.ofNat, HMul.hMul, HAdd.hAdd, 𝕔
9 instances, coercions and auxiliary constants left out.
```
noncomputable def C6_1_2 (a : ℕ) : ℕ := 2 ^ ((𝕔 + 2) * a ^ 3)
```
lemma C6_1_2_ne_zero line 99 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Ne, ENNReal, C6_1_2, OfNat.ofNat
Proof uses: Eq.mpr, HPow.hPow, HMul.hMul, HAdd.hAdd, 𝕔, id, Eq, congrArg, C6_1_2.eq_1, ne_of_gt, Iff.mpr, LT.lt, Nat.cast_pos', pow_pos, inferInstance, PartialOrder, Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool and 1 more
50 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma ineq_6_1_7 line 101 source
lemma norm_Ks_le' Composition of inequalities 6.1.6, 6.1.7, 6.1.8 line 126 source
Source comment
Composition of inequalities 6.1.6, 6.1.7, 6.1.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, 𝔓, Membership.mem, E, Ne, Ks and 14 more
Proof uses: LT.lt, defaultD_pow_pos, mul_defaultD_pow_pos, 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, Int.rawCast, inferInstance, Ring, Int.negOfNat, Nat.rawCast, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl and 135 more
282 instances, coercions and auxiliary constants left out.

Tactic trace: 24 steps
Open to load the checked before-and-after goal states.
```
lemma norm_Ks_le' {x y : X} {𝔄 : Set (𝔓 X)} (p : 𝔄) (hxE : x ∈ E ↑p) (hy : Ks (𝔰 p.1) x y ≠ 0) :
    ‖Ks (𝔰 p.1) x y‖ₑ ≤ 2 ^ (6 * a + (𝕔 + 1) * a ^ 3) / volume (ball (𝔠 p.1) (8 * D ^ 𝔰 p.1)) := by
…
```
Mentions: 𝔓, E, Ks, 𝔰, 𝔠
lemma maximal_bound_antichain Lemma 6.1.2 line 153 source
Source documentation
Lemma 6.1.2.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, IsAntichain, LE.le, Measurable, ENNReal and 10 more
Proof uses: dite, Exists, Ne, carlesonOn, Membership.mem, Eq, Classical.propDecidable, LT.lt, defaultD_pow_pos, mul_defaultD_pow_pos, lt_of_not_ge, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HAdd.hAdd, Neg.neg, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Int.rawCast and 201 more
351 instances, coercions and auxiliary constants left out.

Tactic trace: 68 steps
Open to load the checked before-and-after goal states.
```
lemma maximal_bound_antichain {𝔄 : Set (𝔓 X)} (h𝔄 : IsAntichain (· ≤ ·) 𝔄)
    {f : X → ℂ} (hfm : Measurable f) (x : X) :
    ‖carlesonSum 𝔄 f x‖ₑ ≤ (C6_1_2 a) * maximalFunction volume 𝔄 𝔠 (fun 𝔭 ↦ 8*D ^ 𝔰 𝔭) 1 f x := by
…
```
Mentions: 𝔓, carlesonSum, C6_1_2, 𝔠, 𝔰
def C6_1_3 Constant appearing in Lemma 6.1.3 line 235 source
Source documentation
Constant appearing in Lemma 6.1.3. Has value 2 ^ (103 * 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, 𝕔, Inv.inv, HSub.hSub
24 instances, coercions and auxiliary constants left out.
```
noncomputable def C6_1_3 (a : ℕ) (q : ℝ≥0) : ℝ≥0 := 2 ^ ((𝕔 + 3) * a ^ 3) * (q - 1)⁻¹
…
```
def Lemma6_1_3.𝓜 The maximal function used in the proof of Lemma 6.1.3 line 243 source
Source documentation
The maximal function used in the proof of Lemma 6.1.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, 𝔓, ENNReal
Proof uses: maximalFunction, MeasureTheory.MeasureSpace.volume, 𝔠, HMul.hMul, OfNat.ofNat, HPow.hPow, 𝔰
51 instances, coercions and auxiliary constants left out.
```
def 𝓜 := maximalFunction (ε := ℂ) volume 𝔄 𝔠 (fun 𝔭 ↦ 8 * D ^ 𝔰 𝔭) 1
…
```
Mentions: 𝔠, 𝔰
def Lemma6_1_3.qt $\tilde{q}$ from definition 6.1.10, as a real number line 254 source
Source documentation
$\tilde{q}$ from definition 6.1.10, as a real number.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData
Proof uses: HDiv.hDiv, HMul.hMul, OfNat.ofNat, nnq, HAdd.hAdd
15 instances, coercions and auxiliary constants left out.
```
def qt := (nnqt : ℝ)
```
lemma Lemma6_1_3.inv_qt_eq line 256 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, Eq, Inv.inv, Lemma6_1_3.qt, HAdd.hAdd, OfNat.ofNat, HMul.hMul
Proof uses: inv_nnqt_eq
12 instances, coercions and auxiliary constants left out.
def Lemma6_1_3.p Exponent used for the application of Hölder's inequality in the proof of Lemma 6.1.3 line 259 source
Source documentation
Exponent used for the application of Hölder's inequality in the proof of Lemma 6.1.3.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData
Proof uses: Inv.inv, HSub.hSub, HDiv.hDiv, OfNat.ofNat, Lemma6_1_3.qt
12 instances, coercions and auxiliary constants left out.
```
def p := (3 / 2 - (qt X)⁻¹)⁻¹
```
Mentions: Lemma6_1_3.qt
lemma Lemma6_1_3.inv_p_eq line 261 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, Eq, Inv.inv, Lemma6_1_3.p, HSub.hSub, HDiv.hDiv, OfNat.ofNat, Lemma6_1_3.qt
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, inv_inv, eq_self
32 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Lemma6_1_3.inv_p_eq' line 263 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, Eq, Inv.inv, Lemma6_1_3.p, HSub.hSub, OfNat.ofNat, HMul.hMul
Proof uses: Eq.mpr, HDiv.hDiv, HAdd.hAdd, id, congrFun', congrArg, Eq.trans, Lemma6_1_3.qt, Lemma6_1_3.inv_p_eq, Lemma6_1_3.inv_qt_eq, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Meta.NormNum.instAddMonoidWithOne, HPow.hPow, Rat.rawCast, Int.negOfNat, Mathlib.Tactic.Ring.Common.sub_congr, NNRat.rawCast, Mathlib.Tactic.Ring.Common.div_congr, Mathlib.Tactic.Ring.cast_pos and 51 more
79 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Lemma6_1_3.p_pos line 265 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, LT.lt, OfNat.ofNat, Lemma6_1_3.p
Proof uses: Eq.mpr, HAdd.hAdd, Inv.inv, HMul.hMul, HDiv.hDiv, id, Eq, Eq.trans, HSub.hSub, congrArg, Lemma6_1_3.qt, Lemma6_1_3.inv_qt_eq, LE.le, lt_of_not_ge, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, Neg.neg, inferInstance, AddMonoidWithOne, Mathlib.Meta.NormNum.instAtLeastTwo and 80 more
123 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Lemma6_1_3.one_lt_p line 268 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, LT.lt, OfNat.ofNat, Lemma6_1_3.p
Proof uses: Iff.mp, Inv.inv, Eq.rec, Eq, Iff, inv_lt_inv₀, Lemma6_1_3.p_pos, zero_lt_one, inv_one, HSub.hSub, HMul.hMul, lt_of_not_ge, LE.le, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HAdd.hAdd, Neg.neg, inferInstance, AddMonoidWithOne, Mathlib.Meta.NormNum.instAtLeastTwo and 78 more
104 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Lemma6_1_3.p_lt_two line 271 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, LT.lt, Lemma6_1_3.p, OfNat.ofNat
Proof uses: Iff.mp, Inv.inv, inv_lt_inv₀, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_zero, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Bool, Bool.false, Lemma6_1_3.p_pos, Eq.rec, HSub.hSub, HMul.hMul, Eq, lt_of_not_ge, LE.le, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HAdd.hAdd and 77 more
102 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
def Lemma6_1_3.𝓜p The p maximal function used in the proof line 277 source
Source documentation
The p maximal function used in the proof.

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, 𝔓, ENNReal
Proof uses: maximalFunction, MeasureTheory.MeasureSpace.volume, 𝔠, HMul.hMul, OfNat.ofNat, HPow.hPow, 𝔰, Real.toNNReal
50 instances, coercions and auxiliary constants left out.
```
def 𝓜p (p : ℝ) := maximalFunction volume 𝔄 𝔠 (fun 𝔭 ↦ 8 * D ^ 𝔰 𝔭) p.toNNReal (ε := ℂ)
```
Mentions: Lemma6_1_3.p, 𝔠, 𝔰
lemma Lemma6_1_3.eLpNorm_𝓜p_le Maximal function bound needed in the proof line 280 source
Source documentation
Maximal function bound needed in the proof

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.MemLp, OfNat.ofNat, ENNReal, MeasureTheory.MeasureSpace.volume and 7 more
Proof uses: And.right, MeasureTheory.AEStronglyMeasurable, maximalFunction, 𝔠, HPow.hPow, 𝔰, hasStrongType_maximalFunction, of_eq_true, LT.lt, Eq.trans, True, eq_true, Lemma6_1_3.p_pos, Lemma6_1_3.p_lt_two
115 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma eLpNorm_𝓜p_le (hf : MemLp f 2) :
    eLpNorm (𝓜p 𝔄 (p X) f) 2 ≤ C2_0_6 (defaultA a) (p X).toNNReal 2 * eLpNorm f 2 :=
…
```
Mentions: Lemma6_1_3.𝓜p, Lemma6_1_3.p, defaultA
lemma Lemma6_1_3.eLpNorm_𝓜_le_eLpNorm_𝓜p_mul A maximal function bound via an application of H"older's inequality line 286 source
Source documentation
A maximal function bound via an application of H"older's inequality

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, Measurable, LE.le, Norm.norm, Set.indicator and 11 more
Proof uses: MeasureTheory.BoundedCompactSupport, bcs_of_measurable_of_le_indicator_f, LT.lt, Real.HolderTriple.left_pos, Real.HolderTriple.right_pos, inv_pos_of_pos, Ne, ENNReal.ofReal, Iff.mpr, ENNReal.ofReal_ne_zero_iff, Top.top, ENNReal.ofReal_ne_top, Eq, Real.toNNReal, Real.coe_toNNReal, le_of_lt, Eq.mpr, id, Eq.rec, Eq.refl and 130 more
228 instances, coercions and auxiliary constants left out.

Tactic trace: 67 steps
Open to load the checked before-and-after goal states.
```
lemma eLpNorm_𝓜_le_eLpNorm_𝓜p_mul (hf : Measurable f) (hfF : ∀ x, ‖f x‖ ≤ F.indicator 1 x)
    {p p' : ℝ} (hpp : p.HolderConjugate p') :
    eLpNorm (𝓜 𝔄 f) 2 ≤ (dens₂ 𝔄) ^ (p'⁻¹) * eLpNorm (𝓜p 𝔄 p f) 2 := by
…
```
Mentions: Lemma6_1_3.p, Lemma6_1_3.𝓜, dens₂, Lemma6_1_3.𝓜p
lemma Lemma6_1_3.const_check Tedious check that the constants work out line 359 source
Source documentation
Tedious check that the constants work out.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, LE.le, NNReal, HMul.hMul, C6_1_2, C2_0_6, defaultA, Real.toNNReal, Lemma6_1_3.p, OfNat.ofNat, C6_1_3, nnq
Proof uses: Eq, Real.coe_toNNReal, le_of_lt, Lemma6_1_3.p_pos, LT.lt, Inv.inv, Eq.mpr, HSub.hSub, id, congrArg, Lemma6_1_3.inv_p_eq', le_of_not_gt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HAdd.hAdd, Neg.neg, inferInstance, AddMonoidWithOne, Mathlib.Meta.NormNum.instAtLeastTwo, Mathlib.Tactic.Ring.of_eq and 208 more
211 instances, coercions and auxiliary constants left out.

Tactic trace: 87 steps
Open to load the checked before-and-after goal states.
```
lemma const_check : C6_1_2 a * C2_0_6 (defaultA a) (p X).toNNReal 2 ≤ C6_1_3 a nnq := by
…
```
Mentions: C6_1_2, defaultA, Lemma6_1_3.p, C6_1_3, nnq
lemma dens2_antichain Lemma 6.1.3 (inequality 6.1.11) line 424 source
Source documentation
Lemma 6.1.3 (inequality 6.1.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, 𝔓, IsAntichain, LE.le, Norm.norm, Set.indicator and 19 more
Proof uses: MeasureTheory.BoundedCompactSupport, bcs_of_measurable_of_le_indicator_f, bcs_of_measurable_of_le_indicator_g, le_trans, MeasureTheory.lintegral, MeasureTheory.enorm_integral_le_lintegral_enorm, Eq.mpr, id, Eq, congrFun', congrArg, funext, enorm_mul, Lemma6_1_3.qt, Eq.trans, inv_nnqt_eq, inv_inv, of_eq_true, True, add_sub_cancel_left and 99 more
245 instances, coercions and auxiliary constants left out.

Tactic trace: 28 steps
Open to load the checked before-and-after goal states.
```
lemma dens2_antichain {𝔄 : Set (𝔓 X)} (h𝔄 : IsAntichain (· ≤ ·) 𝔄)
    {f : X → ℂ} (hfF : ∀ x, ‖f x‖ ≤ F.indicator 1 x) (hf : Measurable f)
    {g : X → ℂ} (hgG : ∀ x, ‖g x‖ ≤ G.indicator 1 x) (hg : Measurable g) :
    ‖∫ x, ((starRingEnd ℂ) (g x)) * carlesonSum 𝔄 f x‖ₑ ≤
      (C6_1_3 a nnq) * (dens₂ (𝔄 : Set (𝔓 X))) ^ ((nnqt : ℝ)⁻¹ - 2⁻¹) *
        eLpNorm f 2 * eLpNorm g 2 := by
…
```
Mentions: 𝔓, g, carlesonSum, C6_1_3, nnq, dens₂