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

The iterated derivative is the descending-factorial sum

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

Read this first

Mathematical statement

For every order and point, Mathlib's iterated derivative of the finite series equals the closed polynomial derivative formula.

\[\operatorname{iteratedDeriv}_rP(u)=\sum_{j\in S}j^{\underline r}a_j u^{j-r}\]
Lean statement · iteratedDeriv_finitePowerSeries

This identifies an actual Mathlib derivative, not a merely formal polynomial.

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

Exact module and namespace context

Proof roadmap

  1. 1Commute derivative and finite sum

    Smoothness lets the iterated derivative distribute over all supported monomials.

  2. 2Use Mathlib's monomial formula

    Each term contributes the descending factorial and lowered exponent.

Full assumptions and notation

All objects and hypotheses

  • r is any natural order.
  • u is any real point.
  • The support is finite.

Mathematical proof

1. Commute derivative and finite sum

Smoothness lets the iterated derivative distribute over all supported monomials.

\[D^r\!\left(\sum_j a_j u^j\right)=\sum_j D^r(a_j u^j)\]
Corresponding Lean step

iteratedDeriv_fun_sum supplies the finite-sum rule.

2. Use Mathlib's monomial formula

Each term contributes the descending factorial and lowered exponent.

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

iteratedDeriv_pow gives the exact monomial derivative; ring normalization matches the public definition.

Lean verification

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

Lean proof · iteratedDeriv_finitePowerSeries

The proof reuses Mathlib's finite-sum and power derivative APIs.

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 iteratedDeriv_finitePowerSeries
    (order : ℕ) (support : Finset ℕ) (a : ℕ → ℝ) (u : ℝ) :
    iteratedDeriv order (finitePowerSeries support a) u =
      finitePowerSeriesDerivative order support a u := by
  unfold finitePowerSeries finitePowerSeriesDerivative
  rw [iteratedDeriv_fun_sum]
  · apply Finset.sum_congr rfl
    intro j hj
    simp [iteratedDeriv_pow]
    ring
  · intro j hj
    fun_prop

Exact module and namespace context

Scope and omitted-condition boundaries
  • Only scalar real polynomials are covered.
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.