Carleson/Classical/ClassicalCarleson.lean

GitHub source file

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

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

4 declarations, 0 contain sorry, 0 declared as axioms

Imports (3)
Imported by 2 files
  1. theorem exceptional_set_carleson' TODO: can be removed once two_sided_metric_carleson_hasStrongType no longer depends on sorryAx Theorem 1.1 (Classical Carleson) line 28 source

    Source comment

    TODO: can be removed once `two_sided_metric_carleson_hasStrongType` no longer depends on `sorryAx` Theorem 1.1 (Classical Carleson)

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Real, Complex, Continuous, Function.Periodic, HMul.hMul, OfNat.ofNat, Nat, Real.pi, NNReal, LT.lt, Exists, LE.le, ENNReal, MeasureTheory.distribution, iSup, GT.gt, ENorm.enorm, HSub.hSub, partialFourierSum, MeasureTheory.Measure.restrict and 2 more

    Proof uses: HDiv.hDiv, div_pos, Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Bool, Nat.ble, UniformContinuous, Function.Periodic.uniformContinuous_of_continuous, Real.two_pi_pos, Continuous.continuousOn, Set.Icc, Neg.neg, And, ContDiff, ENat, Top.top, Norm.norm, Min.min and 151 more

    262 instances, coercions and auxiliary constants left out.

    Tactic trace: 77 steps

    Open to load the checked before-and-after goal states.

    theorem exceptional_set_carleson' {f : ℝ → ℂ} (cont_f : Continuous f)
  (periodic_f : f.Periodic (2 * π)) {δ ε : NNReal} (δpos : 0 < δ) (εpos : 0 < ε) :
    ∃ N₀, distribution (fun x ↦ ⨆ N > N₀, ‖f x - S_ N f x‖ₑ) δ (volume.restrict (Set.Ioc 0 (2 * π))) ≤ ε := by
…
  2. theorem carleson_interval' TODO: can be removed once two_sided_metric_carleson_hasStrongType no longer depends on sorryAx line 121 source

    Source comment

    TODO: can be removed once `two_sided_metric_carleson_hasStrongType` no longer depends on `sorryAx`

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Real, Complex, Continuous, Function.Periodic, HMul.hMul, OfNat.ofNat, Nat, Real.pi, Filter.Eventually, Filter.Tendsto, partialFourierSum, Filter.atTop, nhds, MeasureTheory.ae, MeasureTheory.Measure, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, Set.Ioc

    Proof uses: ae_tendsto_zero_of_distribution_le, NNReal, GT.gt, exceptional_set_carleson'

    49 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

    Open to load the checked before-and-after goal states.

    theorem carleson_interval' {f : ℝ → ℂ} (cont_f : Continuous f) (periodic_f : f.Periodic (2 * π)) :
    ∀ᵐ x ∂volume.restrict (Set.Ioc 0 (2 * π)),
      Tendsto (S_ · f x) atTop (𝓝 (f x)) := by
…
  3. theorem classical_carleson Classical Carleson theorem line 131 source

    Source comment

    TODO: can be removed once `two_sided_metric_carleson_hasStrongType` no longer depends on `sorryAx` **Carleson's theorem** asserting a.e. point-wise convergence of the partial Fourier sums for periodic continuous functions.

    L4DEL explanation

    Convergence a.e. on one period, together with periodicity, gives convergence a.e. on the whole real line.

    1. Use periodicity of f and of its partial Fourier sums to reduce a.e. convergence on the line to a.e. convergence on [0, 2*pi].
    2. The a.e. statement on the interval is carleson_interval', which in turn comes from an exceptional-set estimate (exceptional_set_carleson') through a distribution-function criterion for a.e. convergence.
    3. Caveat from the file's own comments: this file is an alternative route kept until two_sided_metric_carleson_hasStrongType no longer depends on sorryAx. A separate derivation, classical_carleson_from_carleson_hunt_real, goes through the general Carleson-Hunt theorem.

    Prerequisites: carleson_interval', exceptional_set_carleson'

    See also: ClassicalCarleson, classical_carleson_from_carleson_hunt_real

    Sources and attribution: Pinned Lean source (8972acdfd953)

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Real, Complex, Continuous, Function.Periodic, HMul.hMul, OfNat.ofNat, Nat, Real.pi, Filter.Eventually, Filter.Tendsto, partialFourierSum, Filter.atTop, nhds, MeasureTheory.ae, MeasureTheory.Measure, MeasureTheory.MeasureSpace.volume

    Proof uses: Function.Periodic.ae_of_ae_restrict, Real.two_pi_pos, Eq.mpr, Eq, HAdd.hAdd, id, congrArg, Function.Periodic.eq_1, congrFun', Filter, funext, Eq.trans, partialFourierSum_periodic, Eq.refl, MeasureTheory.ae_restrict_of_ae_eq_of_ae_restrict, Set.Icc, Set.Ico, Filter.EventuallyEq.symm, MeasureTheory.Ico_ae_eq_Icc, MeasureTheory.Measure.restrict and 5 more

    53 instances, coercions and auxiliary constants left out.

    Tactic trace: 10 steps

    Open to load the checked before-and-after goal states.

    theorem classical_carleson {f : ℝ → ℂ} (cont_f : Continuous f) (periodic_f : f.Periodic (2 * π)) :
    ∀ᵐ x, Tendsto (S_ · f x) atTop (𝓝 (f x)) := by
…
  4. theorem classical_carleson_check line 145 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: ClassicalCarleson

    Proof uses: Real, Complex, classical_carleson