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

10 declarations, 0 contain sorry, 0 declared as axioms

Imports (2)

Imported by 2 files

theorem integrable_tile_sum_operator line 16 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, Measurable, NNReal, defaultA, LE.le, Norm.norm, Set.indicator, OfNat.ofNat, MeasureTheory.Integrable, HMul.hMul, Ks, Complex.exp, Complex.I, HSub.hSub and 4 more
Proof uses: Eq.mpr, id, Eq, congrFun', MeasureTheory.Measure, congrArg, autoParam, funext, mul_assoc, mul_comm, MeasureTheory.Integrable.bdd_mul, integrable_Ks_x, one_lt_realD, Measurable.aestronglyMeasurable, Function.comp, Measurable.mul, Measurable.cexp, Measurable.const_mul, Measurable.sub, Measurable.comp and 29 more
162 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
def 𝔓X_s Used to simplify notation in the proof of tile_sum_operator line 33 source
Source comment
Used to simplify notation in the proof of `tile_sum_operator`
```
private def 𝔓X_s (s : ℤ) := (@Finset.univ (𝔓 X) _).filter (fun p ↦ 𝔰 p = s)
```
Mentions: s, 𝔓, 𝔰
lemma 𝔰_eq line 35 source
lemma 𝔓_biUnion line 38 source
lemma sum_eq_zero_of_notMem_Icc line 46 source
lemma exists_Grid line 56 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, Finset, Set.toFinset, Set.Icc, Exists and 4 more
Proof uses: HPow.hPow, rfl, Metric.ball, HDiv.hDiv, OfNat.ofNat, G_subset, GridStructure.topCube, GridStructure.ball_subset_Grid, Eq.mp, GridStructure.c, congrArg, Eq.symm, GridStructure.s_topCube, GridStructure.c_topCube, dite, Exists.intro, And.intro, Eq.mpr, id, Eq.refl and 19 more
75 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
theorem tile_sum_operator Lemma 4.0.3 line 70 source
Source documentation
Lemma 4.0.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, Membership.mem, SDiff.sdiff, Eq, Finset.sum, 𝔓 and 13 more
Proof uses: Eq.mpr, Finset.biUnion, Classical.propDecidable, Neg.neg, id, congrArg, Finset, Finset.sum_biUnion, Ne, LE.le, False.elim, Bot.bot, Eq.rec, 𝔰, HAdd.hAdd, Finset.filter, Not, Eq.symm, Finset.sum_filter_add_sum_filter_not, OfNat.ofNat and 62 more
146 instances, coercions and auxiliary constants left out.

Tactic trace: 34 steps
Open to load the checked before-and-after goal states.
```
theorem tile_sum_operator {G' : Set X} {f : X → ℂ} {x : X} (hx : x ∈ G \ G') :
    ∑ (p : 𝔓 X), carlesonOn p f x =
    ∑ s ∈ Icc (σ₁ x) (σ₂ x), ∫ y, Ks s x y * f y * exp (I * (Q x y - Q x x)) := by
…
```
Mentions: G', 𝔓, carlesonOn, s, Ks
def C2_0_1 The constant used in Proposition 2.0.1 line 104 source
Source documentation
The constant used in Proposition 2.0.1. Has value 2 ^ (442 * a ^ 3) / (q - 1) ^ 5 in the blueprint.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NNReal
Proof uses: C2_0_2
```
def C2_0_1 (a : ℕ) (q : ℝ≥0) : ℝ≥0 := C2_0_2 a q
```
Mentions: C2_0_2
lemma C2_0_1_pos line 106 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, GT.gt, C2_0_1, nnq, OfNat.ofNat
Proof uses: C2_0_2_pos
29 instances, coercions and auxiliary constants left out.
theorem finitary_carleson Proposition 2.0.1 line 110 source
Source documentation
Proposition 2.0.1

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, Exists, And, MeasurableSet, NNReal, defaultA, LE.le, ENNReal, HMul.hMul, OfNat.ofNat, MeasureTheory.Measure, MeasureTheory.MeasureSpace.volume, Measurable, Norm.norm and 20 more
Proof uses: GridStructure, defaultD, defaultκ, defaultS, cancelPt, grid_existence, TileStructure, tile_existence, carlesonSum, Set.univ, 𝔓, C2_0_2, discrete_carleson, Exists.intro, And.intro, le_of_eq_of_le, MeasureTheory.setLIntegral_congr_fun, MeasurableSet.diff, ProofData.measurableSet_G, Membership.mem and 36 more
233 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
theorem finitary_carleson : ∃ G', MeasurableSet G' ∧ 2 * volume G' ≤ volume G ∧
    ∀ f : X → ℂ, Measurable f → (∀ x, ‖f x‖ ≤ F.indicator 1 x) →
    ∫⁻ x in G \ G', ‖∑ s ∈ Icc (σ₁ x) (σ₂ x), ∫ y, Ks s x y * f y * exp (I * Q x y)‖ₑ ≤
    C2_0_1 a nnq * (volume G) ^ (1 - q⁻¹) * (volume F) ^ q⁻¹ := by
…
```
Mentions: G', s, Ks, C2_0_1, nnq