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

9 declarations, 0 contain sorry, 0 declared as axioms

Imports (4)

Imported by 3 files

lemma close_smooth_approx_periodic line 20 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Complex, UniformContinuous, Function.Periodic, GT.gt, OfNat.ofNat, Exists, And, ContDiff, ENat, Top.top, LE.le, Norm.norm, HSub.hSub
Proof uses: LT.lt, Dist.dist, Iff.mp, Metric.uniformContinuous_iff, ContDiffBump, ContDiffBump.mk, HDiv.hDiv, Nat, lt_of_not_ge, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HAdd.hAdd, HMul.hMul, inferInstance, AddMonoidWithOne, Mathlib.Meta.NormNum.instAtLeastTwo, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HPow.hPow and 102 more
194 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
lemma close_smooth_approx_periodic_Lp line 41 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Fact, LT.lt, OfNat.ofNat, Complex, ENNReal, LE.le, Ne, Top.top, MeasureTheory.MemLp, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, Set.Ioc, NNReal, Exists, And, ContDiff, ENat, Function.Periodic, MeasureTheory.eLpNorm and 1 more
Proof uses: AddCircle, AddCircle.liftIoc, MeasureTheory.MemLp.memLp_liftIoc, Eq.mp, HAdd.hAdd, congrArg, Eq.symm, zero_add, BoundedContinuousFunction, AddSubgroup.zmultiples, HDiv.hDiv, Nat, MeasureTheory.MemLp.exists_boundedContinuous_eLpNorm_sub_le, of_eq_true, Not, Eq, Eq.trans, False, True, Or and 98 more
290 instances, coercions and auxiliary constants left out.

Tactic trace: 57 steps
Open to load the checked before-and-after goal states.
lemma summable_of_le_on_nonzero local lemma line 106 source
Source comment
local lemma

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, Real, LE.le, OfNat.ofNat, Ne, Summable, SummationFilter.unconditional
Proof uses: ite, Eq, rfl, Eq.mpr, id, congrArg, dite, of_eq_true, Eq.trans, True, congr, ite_eq_left_of_eq_true, congrFun', eq_self, Not, False, ite_congr, eq_false, Eq.refl, Summable.of_nonneg_of_le and 13 more
33 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
```
lemma summable_of_le_on_nonzero {f g : ℤ → ℝ} (hgpos : 0 ≤ g) (hgf : ∀ i ≠ 0, g i ≤ f i)
    (summablef : Summable f) : Summable g := by
…
```
Mentions: g
lemma continuous_bounded line 122 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Complex, ContinuousOn, Set.Icc, OfNat.ofNat, HMul.hMul, Nat, Real.pi, Exists, Membership.mem, Set, LE.le, Norm.norm
Proof uses: IsCompact, CompactIccSpace.isCompact_Icc, And, IsMaxOn, Function.comp, IsCompact.exists_isMaxOn, Iff.mpr, Set.Nonempty, Set.nonempty_Icc, LT.lt.le, Real.two_pi_pos, Continuous.comp_continuousOn, continuous_norm, Exists.intro, Eq.mp, congrArg, propext, isMaxOn_iff
70 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma fourierCoeffOn_bound TODO: might be generalized assumptions might be weakened, and constant given explicitely line 132 source
Source comment
TODO: might be generalized assumptions might be weakened, and constant given explicitely

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Complex, Continuous, Exists, Int, LE.le, Norm.norm, fourierCoeffOn, OfNat.ofNat, HMul.hMul, Nat, Real.pi, Real.two_pi_pos
Proof uses: Membership.mem, Set, Set.Icc, continuous_bounded, Continuous.continuousOn, Exists.intro, Eq.mpr, HSMul.hSMul, HDiv.hDiv, HSub.hSub, intervalIntegral, ContinuousMap, AddCircle, AddSubgroup.zmultiples, fourier, Neg.neg, MeasureTheory.MeasureSpace.volume, id, Eq, congrArg and 40 more
159 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
lemma fourierCoeffOn_bound {f : ℝ → ℂ} (f_continuous : Continuous f) :
    ∃ C, ∀ n, ‖fourierCoeffOn Real.two_pi_pos f n‖ ≤ C := by
…
```
lemma periodic_deriv TODO: Assumptions might be weakened line 153 source
Source comment
TODO: Assumptions might be weakened.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NontriviallyNormedField, NormedAddCommGroup, NormedSpace, ContDiff, OfNat.ofNat, WithTop, ENat, Function.Periodic, deriv
Proof uses: HAdd.hAdd, Eq, rfl, Differentiable, Differentiable.add_const, id, differentiable_id, Function.comp, Trans.trans, HSMul.hSMul, deriv.scomp, Differentiable.differentiableAt, ContDiff.differentiable, Mathlib.Meta.NormNum.isNat_eq_false, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_one, Nat.cast_zero, Eq.refl, Bool, Bool.false and 19 more
84 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
```
lemma periodic_deriv {𝕜 : Type} [NontriviallyNormedField 𝕜] {F : Type} [NormedAddCommGroup F] [NormedSpace 𝕜 F]
    {f : 𝕜 → F} {T : 𝕜} (diff_f : ContDiff 𝕜 1 f) (periodic_f : f.Periodic T) : (deriv f).Periodic T := by
…
```
Mentions: T
lemma fourierCoeffOn_ContDiff_two_bound TODO: might be generalized line 170 source
Source comment
TODO: might be generalized. TODO: The assumption periodicf is probably not needed actually.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Complex, Function.Periodic, HMul.hMul, OfNat.ofNat, Nat, Real.pi, ContDiff, WithTop, ENat, Exists, Int, Ne, LE.le, Norm.norm, fourierCoeffOn, Real.two_pi_pos, HDiv.hDiv, HPow.hPow
Proof uses: Membership.mem, Set, Set.uIcc, HasDerivAt, deriv, Eq.mpr, DifferentiableAt, id, Eq, congrArg, propext, hasDerivAt_deriv_iff, ContDiff.differentiable, Mathlib.Meta.NormNum.isNat_eq_false, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Nat.cast_zero, Bool, Bool.false and 152 more
298 instances, coercions and auxiliary constants left out.

Tactic trace: 29 steps
Open to load the checked before-and-after goal states.
```
lemma fourierCoeffOn_ContDiff_two_bound {f : ℝ → ℂ} (periodicf : f.Periodic (2 * π)) (fdiff : ContDiff ℝ 2 f) :
    ∃ C, ∀ n ≠ 0, ‖fourierCoeffOn Real.two_pi_pos f n‖ ≤ C / n ^ 2 := by
…
```
lemma int_sum_nat TODO : Assumptions might be weakened line 204 source
Source comment
TODO : Assumptions might be weakened

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, TopologicalSpace, ContinuousAdd, Int, HasSum, SummationFilter.unconditional, Filter.Tendsto, Nat, Finset.sum, Finset.Icc, Neg.neg, Int.ofNat, Filter.atTop, nhds
Proof uses: HAdd.hAdd, Finset.range, OfNat.ofNat, Filter.Tendsto.add_const, HasSum.tendsto_sum_nat, HasSum.nat_add_neg, Eq.mpr, eq_of_heq, Eq, Filter, HEq, Eq.refl, HEq.refl, Eq.symm, funext, Nat.recAux, of_eq_true, Eq.trans, True, congr and 118 more
146 instances, coercions and auxiliary constants left out.

Tactic trace: 30 steps
Open to load the checked before-and-after goal states.
```
lemma int_sum_nat {β : Type*} [AddCommGroup β] [TopologicalSpace β] [ContinuousAdd β] {f : ℤ → β} {a : β} (hfa : HasSum f a) :
    Filter.Tendsto (fun N ↦ ∑ n ∈ Icc (-Int.ofNat ↑N) N, f n) Filter.atTop (𝓝 a) := by
…
```
lemma fourierConv_ofTwiceDifferentiable line 239 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Complex, Function.Periodic, HMul.hMul, OfNat.ofNat, Nat, Real.pi, ContDiff, WithTop, ENat, GT.gt, Exists, Membership.mem, Set, Set.Icc, LE.le, Norm.norm, HSub.hSub, partialFourierSum
Proof uses: ContinuousMap, AddCircle, AddSubgroup.zmultiples, ContinuousMap.mk, AddCircle.liftIco, instFactLtRealOfNatHMulPi, AddCircle.liftIco_continuous, Eq.symm, HAdd.hAdd, Continuous.continuousOn, ContDiff.continuous, Eq, rfl, LT.lt, lt_of_not_ge, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr and 137 more
281 instances, coercions and auxiliary constants left out.

Tactic trace: 49 steps
Open to load the checked before-and-after goal states.