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

8 declarations, 0 contain sorry, 0 declared as axioms

This file contains a reformulation of Theorem 10.0.1. It is not officially part of the blueprint.

Imports (3)

Imported by 2 files

theorem two_sided_metric_carleson_hasRestrictedWeakType Theorem 10.0.1, reformulation line 27 source
Source comment
Theorem 10.0.1, reformulation

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, MetricSpace, MeasureTheory.DoublingMeasure, NNReal, defaultA, Complex, IsTwoSidedKernel, CompatibleFunctions, Real, IsCancellative, defaultτ, Countable, FunctionDistances.Θ, LE.le, OfNat.ofNat, Membership.mem, Set, Set.Ioc, NNReal.HolderConjugate, GT.gt and 8 more
Proof uses: id, MeasurableSet, LT.lt, MeasureTheory.Measure, Top.top, And.intro, MeasureTheory.AEStronglyMeasurable, Set.indicator, MeasureTheory.eLpNorm, MeasureTheory.Measure.restrict, HMul.hMul, HPow.hPow, ENNReal.toReal, Inv.inv, IsOneSidedKernel, inferInstance, KernelProofData, KernelProofData.mk, Measurable.aestronglyMeasurable, carlesonOperator_measurable and 31 more
162 instances, coercions and auxiliary constants left out.

Tactic trace: 21 steps
Open to load the checked before-and-after goal states.
```
theorem two_sided_metric_carleson_hasRestrictedWeakType [Countable (Θ X)] (ha : 4 ≤ a) (hq : q ∈ Ioc 1 2)
  (hqq' : q.HolderConjugate q')
  (hT : ∀ r > 0, HasBoundedStrongType (czOperator K r) 2 2 volume volume (C_Ts a)) :
      HasRestrictedWeakType (carlesonOperator K) q q' volume volume (C10_0_1 a q) := by
…
```
Mentions: czOperator, K, C_Ts, carlesonOperator, C10_0_1
theorem two_sided_metric_carleson_hasLorentzType line 49 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, MetricSpace, MeasureTheory.DoublingMeasure, NNReal, defaultA, Complex, IsTwoSidedKernel, CompatibleFunctions, Real, IsCancellative, defaultτ, Countable, FunctionDistances.Θ, LE.le, OfNat.ofNat, Membership.mem, Set, Set.Ioo, GT.gt, MeasureTheory.HasBoundedStrongType and 10 more
Proof uses: NNReal.HolderConjugate, NNReal.conjExponent, NNReal.HolderConjugate.conjExponent, And.left, LT.lt, IsOneSidedKernel, inferInstance, KernelProofData, KernelProofData.mk, MeasureTheory.HasRestrictedWeakType.hasLorentzType, Eq.mpr, ENNReal.HolderConjugate, id, Eq, of_eq_true, Not, Eq.trans, False, True, congrArg and 61 more
222 instances, coercions and auxiliary constants left out.

Tactic trace: 54 steps
Open to load the checked before-and-after goal states.
def interpolation_param The parameter where linear interpolation between t₀ and t₁ results in t line 97 source
Source documentation
The parameter where linear interpolation between t₀ and t₁ results in t.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real
Proof uses: HDiv.hDiv, HSub.hSub
5 instances, coercions and auxiliary constants left out.
```
def interpolation_param (t₀ t₁ t : ℝ) := (t - t₀) / (t₁ - t₀)
```
lemma interpolation_param_interpolation TODO: move line 100 source
Source comment
TODO: move

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Ne, Eq, HAdd.hAdd, HMul.hMul, HSub.hSub, OfNat.ofNat, interpolation_param
Proof uses: id, Eq.mpr, HDiv.hDiv, inferInstance, CommGroupWithZero, Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq, Mathlib.Tactic.FieldSimp.NF.eval, Mathlib.Tactic.FieldSimp.NF.cons, Prod.mk, Int, Neg.neg, List.nil, Prod, Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul, rfl, Eq.trans, Eq.refl, Mathlib.Tactic.FieldSimp.NF.atom_eq_eval, Eq.symm, Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg and 66 more
71 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma interpolation_param_interpolation {t₀ t₁ t : ℝ} (h : t₀ ≠ t₁) :
    t = (1 - interpolation_param t₀ t₁ t) * t₀ + interpolation_param t₀ t₁ t * t₁ := by
…
```
Mentions: interpolation_param
lemma interpolation_param_mem_Ioo TODO: move line 106 source
Source comment
TODO: move

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Membership.mem, Set, Set.Ioo, OfNat.ofNat, interpolation_param
Proof uses: LT.lt, LT.lt.trans, And.left, And.right, And.intro, div_pos, HSub.hSub, of_eq_true, Eq.trans, True, HAdd.hAdd, LE.le, eq_true, Eq.mpr, id, Eq, HDiv.hDiv, congrArg, interpolation_param.eq_1, propext and 1 more
72 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
lemma interpolation_param_mem_Ioo {t₀ t₁ t : ℝ} (h : t ∈ Ioo t₀ t₁) :
    interpolation_param t₀ t₁ t ∈ Ioo 0 1 := by
…
```
Mentions: interpolation_param
def C_carleson_hasStrongType The constant used in two_sided_metric_carleson_hasStrongType line 115 source
Source documentation
The constant used in two_sided_metric_carleson_hasStrongType.

depends on sorry what this means
Statement uses: Nat, NNReal
Proof uses: C_LorentzInterpolation, HDiv.hDiv, HAdd.hAdd, OfNat.ofNat, HMul.hMul, C10_0_1, Real.toNNReal, interpolation_param, Inv.inv, Real
20 instances, coercions and auxiliary constants left out.
```
def C_carleson_hasStrongType (a : ℕ) (q : ℝ≥0) :=
…
```
lemma C_carleson_hasStrongType_pos The constant used in two_sided_metric_carleson_hasStrongType line 122 source
Source documentation
The constant used in two_sided_metric_carleson_hasStrongType.

depends on sorry what this means
Statement uses: Nat, NNReal, LT.lt, OfNat.ofNat, C_carleson_hasStrongType
Proof uses: C_LorentzInterpolation_pos, HDiv.hDiv, HAdd.hAdd, HMul.hMul, C10_0_1, Real.toNNReal, interpolation_param, Inv.inv, Real
25 instances, coercions and auxiliary constants left out.
```
lemma C_carleson_hasStrongType_pos {a : ℕ} {q : ℝ≥0} : 0 < C_carleson_hasStrongType a q :=
…
```
Mentions: C_carleson_hasStrongType
theorem two_sided_metric_carleson_hasStrongType Strong-type bound for the Carleson operator (Theorem 10.0.1) line 126 source
Source comment
Theorem 10.0.1, reformulation
L4DEL explanation
Lorentz-type bounds at two exponents bracketing q are combined by real interpolation to give a strong (q,q) bound.
1. Choose two exponents q0 = (q+2)/2 and q1 = (q+1)/2 that bracket q.
2. Obtain Lorentz-type bounds for the Carleson operator at q0 and q1 from two_sided_metric_carleson_hasLorentzType.
3. Apply a real-interpolation theorem for Lorentz spaces (exists_hasLorentzType_real_interpolation) to get HasStrongType with constant C_carleson_hasStrongType.
4. Caveat: the file Classical/ClassicalCarleson.lean says this theorem currently depends on sorryAx, so it is not fully proved in this version.
Prerequisites: C_carleson_hasStrongType, two_sided_metric_carleson_hasLorentzType
See also: classical_carleson
Sources and attribution: Pinned Lean source (8972acdfd953)
depends on sorry what this means
Statement uses: Nat, MetricSpace, MeasureTheory.DoublingMeasure, NNReal, defaultA, Complex, IsTwoSidedKernel, CompatibleFunctions, Real, IsCancellative, defaultτ, Countable, FunctionDistances.Θ, LE.le, OfNat.ofNat, Membership.mem, Set, Set.Ioo, GT.gt, MeasureTheory.HasBoundedStrongType and 7 more
Proof uses: HDiv.hDiv, HAdd.hAdd, Real.toNNReal, interpolation_param, Inv.inv, Eq, Eq.mpr, id, congrArg, Eq.symm, add_div, of_eq_true, Eq.trans, True, add_self_div_two, eq_self, NNReal.eq, Mathlib.Meta.NormNum.instAtLeastTwo, Mathlib.Meta.NormNum.instAddMonoidWithOne', Mathlib.Meta.NormNum.IsNat.to_eq and 102 more
255 instances, coercions and auxiliary constants left out.

Tactic trace: 168 steps
Open to load the checked before-and-after goal states.
```
theorem two_sided_metric_carleson_hasStrongType
  [Countable (Θ X)] (ha : 4 ≤ a) (hq : q ∈ Ioo 1 2)
    (hT : ∀ r > 0, HasBoundedStrongType (czOperator K r) 2 2 volume volume (C_Ts a)) :
      HasStrongType (carlesonOperator K) q q volume volume
        (C_carleson_hasStrongType a q) := by
…
```
Mentions: czOperator, K, C_Ts, carlesonOperator, C_carleson_hasStrongType