`Carleson/ProofData.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

30 declarations, 0 contain sorry, 0 declared as axioms

ProofData.

This file introduces the class ProofData, used to bundle data common through most of chapters 2-7 (except 3), and provides API for it.

Imports (1)

Carleson.DoublingMeasure

Imported by 4 files

class ProofData Data common through most of chapters 2-7 (except 3) line 20 source
Source documentation
Data common through most of chapters 2-7 (except 3).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: outParam, Nat, Real, Complex, Int, Set, PseudoMetricSpace
```
class ProofData {X : Type*} (a : outParam ℕ) (q : outParam ℝ) (K : outParam (X → X → ℂ))
  (σ₁ σ₂ : outParam (X → ℤ)) (F G : outParam (Set X)) [PseudoMetricSpace X] extends
    KernelProofData a K where
…
```
Mentions: K, KernelProofData
lemma S_spec line 50 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, Exists, And, LE.le, Neg.neg, Metric.ball, cancelPt, defaultA, HDiv.hDiv, HPow.hPow, defaultD, OfNat.ofNat, LT.lt
Proof uses: Membership.mem, Set.range, Iff.mp, BddBelow, bddBelow_def, Set.Finite.bddBelow, ProofData.finite_range_σ₁, BddAbove, bddAbove_def, Set.Finite.bddAbove, ProofData.finite_range_σ₂, one_lt_realD, GT.gt, Bornology.IsBounded.subset_ball, ProofData.isBounded_F, Or, lt_or_ge, Exists.intro, And.intro, zero_lt_one and 118 more
206 instances, coercions and auxiliary constants left out.

Tactic trace: 58 steps
Open to load the checked before-and-after goal states.
def defaultS line 99 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData
Proof uses: Nat.find, And, LE.le, Neg.neg, Metric.ball, cancelPt, defaultA, HDiv.hDiv, HPow.hPow, defaultD, OfNat.ofNat, LT.lt, Classical.propDecidable, S_spec
22 instances, coercions and auxiliary constants left out.
lemma range_σ₁_subset line 101 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, LE.le, Set.range, Set.Icc, Neg.neg, defaultS
Proof uses: Eq.mpr, Membership.mem, id, Eq, congrArg, propext, Set.range_subset_iff, And, Nat.find, Metric.ball, cancelPt, defaultA, HDiv.hDiv, HPow.hPow, defaultD, OfNat.ofNat, LT.lt, Classical.propDecidable, S_spec, And.left and 5 more
41 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma range_σ₂_subset line 107 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, LE.le, Set.range, Set.Icc, Neg.neg, defaultS
Proof uses: Eq.mpr, Membership.mem, id, Eq, congrArg, propext, Set.range_subset_iff, And, Nat.find, Metric.ball, cancelPt, defaultA, HDiv.hDiv, HPow.hPow, defaultD, OfNat.ofNat, LT.lt, Classical.propDecidable, S_spec, And.left and 5 more
41 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma F_subset line 113 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, LE.le, Metric.ball, cancelPt, defaultA, HDiv.hDiv, HPow.hPow, defaultD, defaultS, OfNat.ofNat
Proof uses: And.left, Nat.find, And, Neg.neg, LT.lt, Classical.propDecidable, S_spec, And.right, Nat.find_spec
40 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma G_subset line 116 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, LE.le, Metric.ball, cancelPt, defaultA, HDiv.hDiv, HPow.hPow, defaultD, defaultS, OfNat.ofNat
Proof uses: And.left, Nat.find, And, Neg.neg, LT.lt, Classical.propDecidable, S_spec, And.right, Nat.find_spec
40 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma defaultS_pos line 119 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, LT.lt, OfNat.ofNat, defaultS
Proof uses: And.right, LE.le, Metric.ball, cancelPt, defaultA, HDiv.hDiv, HPow.hPow, defaultD, Nat.find, And, Neg.neg, Classical.propDecidable, S_spec, Nat.find_spec
25 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Icc_σ_subset_Icc_S line 122 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, LE.le, Set.Icc, Neg.neg, defaultS
Proof uses: Membership.mem, And.intro, LE.le.trans, And.left, range_σ₁_subset, Exists.intro, Eq, rfl, And.right, range_σ₂_subset
21 instances, coercions and auxiliary constants left out.
lemma one_lt_q line 127 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, LT.lt, OfNat.ofNat
Proof uses: And.left, outParam, LE.le, ProofData.q_mem_Ioc
13 instances, coercions and auxiliary constants left out.
lemma q_le_two line 128 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, LE.le, OfNat.ofNat
Proof uses: And.right, LT.lt, outParam, ProofData.q_mem_Ioc
16 instances, coercions and auxiliary constants left out.
lemma q_pos line 129 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, LT.lt, OfNat.ofNat
Proof uses: LT.lt.trans, zero_lt_one, one_lt_q
19 instances, coercions and auxiliary constants left out.
lemma q_nonneg line 130 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, LE.le, OfNat.ofNat
Proof uses: LT.lt.le, q_pos
6 instances, coercions and auxiliary constants left out.
lemma inv_q_sub_half_nonneg line 131 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, LE.le, OfNat.ofNat, HSub.hSub, Inv.inv
Proof uses: of_eq_true, Eq.trans, True, propext, inv_le_inv₀, zero_lt_two, q_pos, eq_true, q_le_two
67 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma inv_q_mem_Ico Note: For exponent computations it is usually cleaner to argue in terms of q⁻¹ rather than q, both on paper and in Lean line 136 source
Source comment
Note: For exponent computations it is usually cleaner to argue in terms of `q⁻¹` rather than `q`, both on paper and in Lean.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, Membership.mem, Set.Ico, Inv.inv, OfNat.ofNat
Proof uses: And.intro, LE.le, LT.lt, le_of_not_gt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HAdd.hAdd, HSub.hSub, HMul.hMul, inferInstance, AddMonoidWithOne, Mathlib.Meta.NormNum.instAtLeastTwo, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Int.rawCast, Ring, Int.negOfNat, HPow.hPow, Nat.rawCast and 75 more
104 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma inv_q_mem_Ico : q⁻¹ ∈ Ico 2⁻¹ 1 := ⟨by linarith only [inv_q_sub_half_nonneg X],
…
```
Mentions: inv_q_sub_half_nonneg
def nnq q as an element of ℝ≥0 line 140 source
Source documentation
q as an element of ℝ≥0.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, NNReal
Proof uses: Subtype.mk, LE.le, OfNat.ofNat, q_nonneg
3 instances, coercions and auxiliary constants left out.
```
def nnq : ℝ≥0 := ⟨q, q_nonneg X⟩
```
Mentions: q_nonneg
lemma one_lt_nnq line 142 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, LT.lt, NNReal, OfNat.ofNat, nnq
Proof uses: one_lt_q
5 instances, coercions and auxiliary constants left out.
lemma nnq_le_two line 143 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, LE.le, NNReal, nnq, OfNat.ofNat
Proof uses: q_le_two
12 instances, coercions and auxiliary constants left out.
lemma nnq_pos line 144 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, LT.lt, NNReal, OfNat.ofNat, nnq
Proof uses: q_pos
5 instances, coercions and auxiliary constants left out.
lemma nnq_mem_Ioc line 145 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, Membership.mem, NNReal, Set.Ioc, OfNat.ofNat, nnq
Proof uses: And.intro, LT.lt, LE.le, Iff.mp, NNReal.coe_lt_coe, And.left, outParam, ProofData.q_mem_Ioc, NNReal.coe_le_coe, And.right
35 instances, coercions and auxiliary constants left out.
lemma two_le_κZ Used in third_exception (Lemma 5.2.10) line 163 source
Source documentation
Used in third_exception (Lemma 5.2.10).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, LE.le, OfNat.ofNat, HMul.hMul, defaultκ, defaultZ
Proof uses: Eq.mpr, HPow.hPow, Neg.neg, id, Eq, congrArg, defaultκ.eq_1, defaultZ.eq_1, Nat.cast_pow, Eq.refl, Eq.trans, congr, Real.rpow_natCast, HAdd.hAdd, Eq.symm, Real.rpow_add, zero_lt_two, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Meta.NormNum.instAddMonoidWithOne and 63 more
124 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
lemma two_le_κZ [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] : 2 ≤ κ * Z := by
…
```
Mentions: ProofData, K
lemma DκZ_le_two_rpow_100 Used in third_exception (Lemma 5.2.10) line 171 source
Source documentation
Used in third_exception (Lemma 5.2.10).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, LE.le, ENNReal, HPow.hPow, defaultD, HMul.hMul, Neg.neg, defaultκ, defaultZ, OfNat.ofNat
Proof uses: Eq.mpr, 𝕔, id, Eq, congrArg, defaultD.eq_1, Nat.cast_pow, Eq.symm, ENNReal.rpow_natCast, ENNReal.rpow_mul, Eq.refl, ENNReal.rpow_le_rpow_of_exponent_le, one_le_two, defaultκ.eq_1, defaultZ.eq_1, neg_mul, Eq.trans, congr, Real.rpow_natCast, mul_neg and 80 more
158 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
```
lemma DκZ_le_two_rpow_100 [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] :
    (D : ℝ≥0∞) ^ (-κ * Z) ≤ 2 ^ (-100 : ℝ) := by
…
```
Mentions: ProofData, K
lemma four_le_Z line 189 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, LE.le, OfNat.ofNat, defaultZ
Proof uses: Eq.mpr, HPow.hPow, HMul.hMul, id, Eq, congrArg, defaultZ.eq_1, Eq.refl, Nat.pow_le_pow_right, zero_lt_two, le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HAdd.hAdd, Neg.neg, HSub.hSub, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Int.rawCast and 55 more
85 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma volume_F_lt_top line 197 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, LT.lt, ENNReal, MeasureTheory.Measure, NNReal, defaultA, MeasureTheory.MeasureSpace.volume, Top.top
Proof uses: Bornology.IsBounded.measure_lt_top, ProofData.isBounded_F
38 instances, coercions and auxiliary constants left out.
lemma volume_F_ne_top line 198 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, Ne, ENNReal, MeasureTheory.Measure, NNReal, defaultA, MeasureTheory.MeasureSpace.volume, Top.top
Proof uses: LT.lt.ne, volume_F_lt_top
28 instances, coercions and auxiliary constants left out.
lemma volume_G_lt_top line 199 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, LT.lt, ENNReal, MeasureTheory.Measure, NNReal, defaultA, MeasureTheory.MeasureSpace.volume, Top.top
Proof uses: Bornology.IsBounded.measure_lt_top, ProofData.isBounded_G
38 instances, coercions and auxiliary constants left out.
lemma volume_G_ne_top line 200 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, Ne, ENNReal, MeasureTheory.Measure, NNReal, defaultA, MeasureTheory.MeasureSpace.volume, Top.top
Proof uses: LT.lt.ne, volume_G_lt_top
28 instances, coercions and auxiliary constants left out.
def C2_1_1 line 204 source
standard axioms: propext what this means
Statement uses: Nat
Proof uses: HPow.hPow, OfNat.ofNat, HMul.hMul
7 instances, coercions and auxiliary constants left out.
lemma Θ.finite_and_mk_le_of_le_dist line 207 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, FunctionDistances.Θ, defaultA, LE.le, Metric.ball, WithFunctionDistance, HMul.hMul, HPow.hPow, OfNat.ofNat, Set.PairwiseDisjoint, And, Set.Finite, Cardinal, Cardinal.mk and 1 more
Proof uses: CoveredByBalls, ballsCoverBalls_iterate_nat, Finset, Finset.card, Set.iUnion, Membership.mem, Finset.filter, Classical.propDecidable, Ne, Iff.mpr, Disjoint, Not, Finset.disjoint_filter, Iff.mp, Set.disjoint_left, Eq.mp, congrArg, propext, Metric.mem_ball_comm, Finset.Nonempty and 61 more
137 instances, coercions and auxiliary constants left out.

Tactic trace: 35 steps
Open to load the checked before-and-after goal states.
lemma Θ.card_le_of_le_dist line 249 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, FunctionDistances.Θ, defaultA, LE.le, Metric.ball, WithFunctionDistance, HMul.hMul, HPow.hPow, OfNat.ofNat, Set.PairwiseDisjoint, Nat.card, C2_1_1
Proof uses: Set.Finite, Cardinal, Cardinal.mk, And, Θ.finite_and_mk_le_of_le_dist, Finset, Eq, Exists, CanLift.prf, Eq.mpr, Finset.card, id, congrFun', congrArg, Eq.trans, Subtype, Membership.mem, Fintype.card, Nat.card_eq_fintype_card, Fintype.card_coe and 2 more
86 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.