Samplinglib mathematical lesson

Signed derivative budgets on the unit interval

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

Read this first

Mathematical statement

On |u|≤1, every iterated derivative is bounded by its weighted absolute coefficient mass.

\[|u|\le1\Longrightarrow |P^{(r)}(u)|\le M_r\]

Lean statement · abs_iteratedDeriv_finitePowerSeries_le_mass

Low degrees and coefficient signs remain inside the theorem.

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 abs_iteratedDeriv_finitePowerSeries_le_mass
    (order : ℕ) (support : Finset ℕ) (a : ℕ → ℝ) {u : ℝ}
    (hu : |u| ≤ 1) :
    |iteratedDeriv order (finitePowerSeries support a) u| ≤
      finitePowerSeriesDerivativeMass order support a

Exact module and namespace context

Proof roadmap

1Insert the exact derivative
Rewrite the actual derivative as the descending-factorial finite sum.
2Apply the triangle inequality
Discard cancellation and split absolute values across products.
3Use |u|≤1
Every remaining power is at most one.

Full assumptions and notation

All objects and hypotheses

u lies in [-1,1].
The derivative order is arbitrary.
Coefficients may have arbitrary signs.

Mathematical proof

1. Insert the exact derivative

Rewrite the actual derivative as the descending-factorial finite sum.

\[P^{(r)}(u)=\sum_j j^{\underline r}a_j u^{j-r}\]

Corresponding Lean step

Use iteratedDeriv_finitePowerSeries.

2. Apply the triangle inequality

Discard cancellation and split absolute values across products.

\[|P^{(r)}(u)|\le\sum_j j^{\underline r}|a_j||u|^{j-r}\]

Corresponding Lean step

Finset.abs_sum_le_sum_abs proves the finite-sum bound.

3. Use |u|≤1

Every remaining power is at most one.

\[|u|^{j-r}\le1\Longrightarrow |P^{(r)}(u)|\le M_r\]

Corresponding Lean step

pow_le_one₀ completes the comparison.

Lean verification

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

Lean proof · abs_iteratedDeriv_finitePowerSeries_le_mass

The proof combines the exact derivative identity with elementary absolute-value estimates.

Download module (.lean)

theorem abs_iteratedDeriv_finitePowerSeries_le_mass
    (order : ℕ) (support : Finset ℕ) (a : ℕ → ℝ) {u : ℝ}
    (hu : |u| ≤ 1) :
    |iteratedDeriv order (finitePowerSeries support a) u| ≤
      finitePowerSeriesDerivativeMass order support a := by
  rw [iteratedDeriv_finitePowerSeries]
  unfold finitePowerSeriesDerivative finitePowerSeriesDerivativeMass
  calc
    |∑ j ∈ support,
        (j.descFactorial order : ℝ) * a j * u ^ (j - order)| ≤
        ∑ j ∈ support,
          |(j.descFactorial order : ℝ) * a j * u ^ (j - order)| :=
      Finset.abs_sum_le_sum_abs _ _
    _ = ∑ j ∈ support,
        (j.descFactorial order : ℝ) * |a j| * |u| ^ (j - order) := by
      apply Finset.sum_congr rfl
      intro j hj
      rw [abs_mul, abs_mul, abs_pow,
        abs_of_nonneg (show 0 ≤ (j.descFactorial order : ℝ) by positivity)]
    _ ≤ ∑ j ∈ support, (j.descFactorial order : ℝ) * |a j| := by
      apply Finset.sum_le_sum
      intro j hj
      exact mul_le_of_le_one_right
        (mul_nonneg (by positivity) (abs_nonneg (a j)))
        (pow_le_one₀ (abs_nonneg u) hu)

Exact module and namespace context

Scope and omitted-condition boundaries

Outside [-1,1], a radius-dependent budget is needed.

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 compiled source — Exact statement and proof.

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