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

The closed formula for every derivative order

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

Read this first

Mathematical statement

The order-r derivative expression weights u^(j-r) by the descending factorial j^(r) and the original coefficient.

\[P_r(u)=\sum_{j\in S}j^{\underline r}a_j u^{j-r}\]
Lean statement · finitePowerSeriesDerivative

The order is explicit and the result is real-valued.

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

Exact module and namespace context

Proof roadmap

  1. 1Differentiate each monomial formally

    The r-th derivative of u^j is j falling r times u^(j-r), including the zero case j<r.

Full assumptions and notation

All objects and hypotheses

  • r and j are natural numbers.
  • Natural subtraction is truncated.
  • When j<r, the descending factorial is zero.

Construction and meaning

1. Differentiate each monomial formally

The r-th derivative of u^j is j falling r times u^(j-r), including the zero case j<r.

\[D^r(u^j)=j^{\underline r}u^{j-r}\]
Corresponding Lean step

Nat.descFactorial handles all orders uniformly.

Lean verification

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

Lean construction · finitePowerSeriesDerivative

The later theorem identifies this expression with Mathlib's actual iterated derivative.

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

Exact module and namespace context

Scope and omitted-condition boundaries
  • This definition alone does not assert differentiability.
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.