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

12 declarations, 0 contain sorry, 0 declared as axioms

Imports (1)

Carleson.Classical.Basic

Imported by 3 files

def k line 14 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Complex
Proof uses: HDiv.hDiv, Max.max, HSub.hSub, OfNat.ofNat, abs, Complex.exp, HMul.hMul, Complex.I
17 instances, coercions and auxiliary constants left out.
lemma k_of_neg_eq_conj_k line 18 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Eq, Complex, k, Neg.neg, RingHom, starRingEnd
Proof uses: of_eq_true, Eq.trans, HDiv.hDiv, Max.max, HSub.hSub, OfNat.ofNat, abs, Complex.exp, HMul.hMul, Complex.I, True, congr, congrArg, congrFun', abs_neg, Complex.ofReal_neg, mul_neg, map_div₀, Complex.conj_ofReal, map_sub and 7 more
79 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma k_of_abs_le_one line 21 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LE.le, abs, OfNat.ofNat, Eq, Complex, k, HDiv.hDiv, HSub.hSub, Complex.exp, HMul.hMul, Complex.I
Proof uses: Eq.mpr, id, Eq.trans, Nat, congrArg, congr, congrFun', Eq.symm, Nat.cast_one, Max.max, k.eq_1, Nat.cast_zero, max_eq_left, le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HAdd.hAdd, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr and 36 more
88 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma k_of_one_le_abs line 24 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LE.le, OfNat.ofNat, abs, Eq, Complex, k
Proof uses: Eq.mpr, HDiv.hDiv, Max.max, HSub.hSub, Complex.exp, HMul.hMul, Complex.I, id, congrArg, k.eq_1, max_eq_right, le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HAdd.hAdd, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Nat.rawCast, HPow.hPow and 44 more
77 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma k_measurable line 29 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Measurable, Real, Complex, k
Proof uses: id, Measurable.fun_div, Max.max, HSub.hSub, OfNat.ofNat, abs, Complex.exp, HMul.hMul, Complex.I, Measurable.complex_ofReal, Measurable.sup_const, Measurable.const_sub, Continuous.measurable, Continuous.abs, continuous_id', Measurable.cexp, Measurable.const_mul, measurable_id'
83 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
def K line 33 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Complex
Proof uses: k, HSub.hSub
2 instances, coercions and auxiliary constants left out.
lemma K_def line 35 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Real, Complex, K, k, HSub.hSub
Proof uses: rfl
2 instances, coercions and auxiliary constants left out.
lemma Hilbert_kernel_conj_symm line 37 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Eq, Complex, K, RingHom, starRingEnd
Proof uses: Eq.mpr, k, HSub.hSub, id, congrArg, K.eq_1, Neg.neg, Eq.symm, neg_sub, k_of_neg_eq_conj_k, Eq.refl
21 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Hilbert_kernel_measurable line 41 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Measurable, Prod, Real, Complex, Function.uncurry, K
Proof uses: Measurable.comp, k, HSub.hSub, Prod.fst, Prod.snd, k_measurable, MeasurableSub₂.measurable_sub
17 instances, coercions and auxiliary constants left out.
lemma Hilbert_kernel_bound Lemma 11.1.11 (Hilbert kernel bound) line 45 source
Source comment
Lemma 11.1.11 (Hilbert kernel bound)

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LE.le, Norm.norm, Complex, K, HDiv.hDiv, HPow.hPow, OfNat.ofNat, Nat, HMul.hMul, abs, HSub.hSub
Proof uses: dite, And, LT.lt, Trans.trans, Eq, Complex.exp, Complex.I, rfl, Eq.mpr, k, id, congrArg, K.eq_1, Max.max, k.eq_1, norm_div, div_le_div_of_nonneg_right, Complex.norm_real, Real.norm_eq_abs, abs_of_nonneg and 158 more
199 instances, coercions and auxiliary constants left out.

Tactic trace: 50 steps
Open to load the checked before-and-after goal states.
```
lemma Hilbert_kernel_bound {x y : ℝ} : ‖K x y‖ ≤ 2 ^ (2 : ℝ) / (2 * |x - y|) := by
…
```
Mentions: K
lemma Hilbert_kernel_regularity_main_part Main part of the proof of Hilbert_kernel_regularity TODO: This can be local, i.e. invisible to other files line 87 source
Source comment
Main part of the proof of Hilbert_kernel_regularity TODO: This can be local, i.e. invisible to other files.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, And, LE.le, OfNat.ofNat, LT.lt, HDiv.hDiv, Nat, Norm.norm, Complex, HSub.hSub, k, Neg.neg, HMul.hMul, HPow.hPow, abs
Proof uses: Eq.mpr, Complex.exp, Complex.I, id, Eq, congrArg, k_of_abs_le_one, abs_neg, abs_of_nonneg, And.left, And.right, congrFun', congr, Eq.trans, Complex.ofReal_neg, mul_neg, rfl, HAdd.hAdd, Membership.mem, Set and 249 more
319 instances, coercions and auxiliary constants left out.

Tactic trace: 134 steps
Open to load the checked before-and-after goal states.
```
lemma Hilbert_kernel_regularity_main_part {y y' : ℝ} (yy'nonneg : 0 ≤ y ∧ 0 ≤ y') (ypos : 0 < y)
    (y2ley' : y / 2 ≤ y') (hy : y ≤ 1) (hy' : y' ≤ 1) :
    ‖k (-y) - k (-y')‖ ≤ 2 ^ 6 * (1 / |y|) * (|y - y'| / |y|) := by
…
```
Mentions: k
lemma Hilbert_kernel_regularity Lemma 11.1.12 (Hilbert kernel regularity) line 208 source
Source comment
Lemma 11.1.12 (Hilbert kernel regularity)

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LE.le, HMul.hMul, OfNat.ofNat, Nat, abs, HSub.hSub, Norm.norm, Complex, K, HPow.hPow, HDiv.hDiv
Proof uses: Eq.mpr, k, id, Eq, congrArg, K.eq_1, Not, Or, Classical.em, Neg.neg, congr, zero_sub, Eq.trans, abs_neg, And, dite, le_antisymm, And.left, Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt, Not.intro and 183 more
222 instances, coercions and auxiliary constants left out.

Tactic trace: 126 steps
Open to load the checked before-and-after goal states.
```
lemma Hilbert_kernel_regularity {x y y' : ℝ} :
    2 * |y - y'| ≤ |x - y| → ‖K x y - K x y'‖ ≤ 2 ^ 8 * (1 / |x - y|) * (|y - y'| / |x - y|)  := by
…
```
Mentions: K