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

A finite real power series

AutoSamplingTheory.TechnicalLemmas.Analysis.FinitePowerSeries.finitePowerSeries · def · Teaching coverage

Read this first

Mathematical statement

A finite set of natural exponents and arbitrary real coefficients define a polynomial by summing the supported monomials.

\[P(u)=\sum_{j\in S}a_j u^j\]
Lean statement · finitePowerSeries

Lean records the support, coefficient family, and evaluation point explicitly.

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)
def finitePowerSeries (support : Finset ℕ) (a : ℕ → ℝ) (u : ℝ) : ℝ

Exact module and namespace context

Proof roadmap

  1. 1Build the finite sum

    Evaluate a_j u^j for every supported exponent and add the results. No convergence hypothesis is needed because the support is finite.

Full assumptions and notation

All objects and hypotheses

  • S is finite.
  • Coefficients may have any signs.
  • u is real.

Construction and meaning

1. Build the finite sum

Evaluate a_j u^j for every supported exponent and add the results. No convergence hypothesis is needed because the support is finite.

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

The definition is a Finset.sum.

Lean verification

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

Lean construction · finitePowerSeries

This is the complete construction, rather than a proof of another claim.

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)
def finitePowerSeries (support : Finset ℕ) (a : ℕ → ℝ) (u : ℝ) : ℝ :=
  ∑ j ∈ support, a j * u ^ j

Exact module and namespace context

Scope and omitted-condition boundaries
  • No canonical support or infinite-series statement is asserted.
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.