derivative_amplitude_sum
plain-language theorem explainer
derivative_amplitude_sum defines the summed quantity of absolute products |a_k ω_k| over the first n indices, supplying the left-hand side for the finite Bernstein derivative bound. Analysts constructing explicit Mathlib proofs for trigonometric polynomials in the Recognition Science analysis module cite it when building certificates that replace axiomatic Bernstein statements. The definition is a direct Finset summation of absolute values with no additional lemmas required.
Claim. For sequences $a, ω : ℕ → ℝ$ and $n ∈ ℕ$, the derivative amplitude sum is defined as $∑_{k=0}^{n-1} |a(k) ⋅ ω(k)|$.
background
The Bernstein Inequality module supplies Mathlib-native proofs for the finite trigonometric polynomial version of Bernstein's inequality, replacing the three listed axioms (bernstein_pointwise_axiom, bernstein_inequality_finite_axiom, far_field_zero_free_axiom) with explicit constructions. In this setting a finite sum with frequencies bounded by Ω obeys ‖f'‖∞ ≤ Ω ‖f‖∞, where amplitude_sum a n := ∑_{k<n} |a k| serves as a proxy for the sup-norm of the function and FrequencyBounded ω n Ω asserts |ω k| ≤ Ω for each k < n.
proof idea
This is a direct definition that expands to the Finset sum over range n of |a k * ω k|. It is invoked in derivative_bounded_by_frequency by simultaneous unfolding of both derivative_amplitude_sum and amplitude_sum, followed by rw [Finset.mul_sum] and application of Finset.sum_le_sum.
why it matters
The definition is a component of BernsteinCert (which packages amplitude nonnegativity and the derivative bound under FrequencyBounded) and directly enables the theorem derivative_bounded_by_frequency that proves the finite Bernstein inequality. It advances the module goal of eliminating the Bernstein axioms in favor of constructive Mathlib proofs, supporting the Recognition Science treatment of bandlimited functions. The work touches the open question of fully embedding classical inequalities into the core RS derivations without external axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.