Samplinglib
Lean gate not recorded for this source state main · 9bb7a7394ab0
Samplinglib mathematical lesson

Finite power series are smooth

AutoSamplingTheory.TechnicalLemmas.Analysis.FinitePowerSeries.finitePowerSeries_contDiff · theorem · Teaching coverage

Read this first

Mathematical statement

Every finite real power series is continuously differentiable to all finite orders.

\[P\in C^\infty(\mathbb R;\mathbb R)\]
Lean statement · finitePowerSeries_contDiff

The conclusion is Mathlib's `ContDiff ℝ ⊤`.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

Download module (.lean)
theorem finitePowerSeries_contDiff
    (support : Finset ℕ) (a : ℕ → ℝ) :
    ContDiff ℝ ⊤ (finitePowerSeries support a)

Exact module and namespace context

Proof roadmap

  1. 1Use closure of smooth functions

    Each monomial is smooth; constant multiples and finite sums preserve smoothness.

Full assumptions and notation

All objects and hypotheses

  • The exponent support is finite.
  • Coefficients are arbitrary reals.

Mathematical proof

1. Use closure of smooth functions

Each monomial is smooth; constant multiples and finite sums preserve smoothness.

\[P=\sum_{j\in S}(u\mapsto a_j u^j)\in C^\infty\]
Corresponding Lean step

After unfolding the definition, fun_prop applies Mathlib's closure rules.

Lean verification

The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.

Lean proof · finitePowerSeries_contDiff

The proof uses only standard smoothness rules.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

Download module (.lean)
theorem finitePowerSeries_contDiff
    (support : Finset ℕ) (a : ℕ → ℝ) :
    ContDiff ℝ ⊤ (finitePowerSeries support a) := by
  unfold finitePowerSeries
  fun_prop

Exact module and namespace context

Scope and omitted-condition boundaries
  • No infinite-series analyticity claim is made.
Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

    Mathlib API called (external library)

    No direct Mathlib call recorded; see the Samplinglib parents.

    Mathematical sources

    Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.