Carleson/Classical/CarlesonHuntBasic.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

2 declarations, 0 contain sorry, 0 declared as axioms

Imports (2)
Imported by 3 files
  1. lemma ae_tendsto_zero_of_distribution_le TODO: generalize and clean this up line 15 source

    Source comment

    TODO: generalize and clean this up

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

    Statement uses: MeasurableSpace, MeasureTheory.Measure, Complex, Nat, NNReal, GT.gt, OfNat.ofNat, Exists, LE.le, ENNReal, MeasureTheory.distribution, iSup, ENorm.enorm, HSub.hSub, Filter.Eventually, Filter.Tendsto, Filter.atTop, nhds, MeasureTheory.ae

    Proof uses: Real, HDiv.hDiv, HAdd.hAdd, tendsto_one_div_add_atTop_nhds_zero_nat, Rat, NNRat, LT.lt, div_pos, zero_lt_one, lt_of_not_ge, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, Neg.neg, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Int.rawCast, inferInstance, Ring, Int.negOfNat and 181 more

    292 instances, coercions and auxiliary constants left out.

    Tactic trace: 101 steps

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

    lemma ae_tendsto_zero_of_distribution_le {α : Type*} {m : MeasurableSpace α} {μ : Measure α}
  {f : α → ℂ} {F : ℕ → α → ℂ}
  (h : ∀ δ > (0 : NNReal), ∀ ε > (0 : NNReal), ∃ N₀,
    distribution (fun x ↦ ⨆ N > N₀, ‖f x - F N x‖ₑ) δ μ ≤ ε) :
    ∀ᵐ x ∂μ, Tendsto (F · x) atTop (𝓝 (f x)) := by
…
  2. lemma Function.Periodic.ae_of_ae_restrict TODO: might be generalized line 121 source

    Source comment

    TODO: might be generalized

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

    Statement uses: Real, LT.lt, OfNat.ofNat, Function.Periodic, Filter.Eventually, MeasureTheory.ae, MeasureTheory.Measure, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, Set.Ico, HAdd.hAdd

    Proof uses: Set, Set.ofPred, Not, Membership.mem, Eq, rfl, Set.iUnion, Int, HVAdd.hVAdd, Set.vaddSet, HSMul.hSMul, Set.ext, Eq.mpr, Iff, Exists, id, congrArg, propext, Set.mem_iUnion, Iff.intro and 23 more

    84 instances, coercions and auxiliary constants left out.

    Tactic trace: 26 steps

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

    lemma Function.Periodic.ae_of_ae_restrict {T : ℝ} (hT : 0 < T) {a : ℝ} {P : (x : ℝ) → Prop}
    (hP : Function.Periodic P T)
    (h : ∀ᵐ x ∂volume.restrict (Set.Ico a (a + T)), P x) : ∀ᵐ x, P x := by
…

    Mentions: T