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

An absolute coefficient budget

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

Read this first

Mathematical statement

Replace each coefficient by its absolute value and retain the derivative's descending-factorial weight.

\[M_r=\sum_{j\in S}j^{\underline r}|a_j|\]
Lean statement · finitePowerSeriesDerivativeMass

The mass depends on order, support, and coefficients, but not u.

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

Exact module and namespace context

Proof roadmap

  1. 1Discard cancellation

    Summing absolute coefficient contributions produces a point-independent majorant.

Full assumptions and notation

All objects and hypotheses

  • The support is finite.
  • No coefficient sign condition is used.
  • Every summand is nonnegative.

Construction and meaning

1. Discard cancellation

Summing absolute coefficient contributions produces a point-independent majorant.

\[M_r=\sum_{j\in S}j^{\underline r}|a_j|\]
Corresponding Lean step

The definition is a finite sum of nonnegative real terms.

Lean verification

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

Lean construction · finitePowerSeriesDerivativeMass

It is designed to pair with the hypothesis |u|≤1.

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

Exact module and namespace context

Scope and omitted-condition boundaries
  • The budget need not be sharp.
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.