amplitude_sum_nonneg
plain-language theorem explainer
The non-negativity of the finite sum of absolute amplitudes holds for any real-valued sequence and length. Analysts replacing Bernstein inequality axioms with explicit Mathlib proofs cite this when assembling certificates for derivative bounds on trigonometric polynomials. The proof is a one-line term that unfolds the sum definition and applies the standard non-negativity lemma for Finset sums of absolute values.
Claim. $0 ≤ ∑_{k=0}^{n-1} |a(k)|$ for any $a:ℕ→ℝ$ and $n:ℕ$.
background
The BernsteinInequality module supplies Mathlib proofs for the finite trigonometric polynomial case of Bernstein's inequality, targeting replacement of the three listed axioms including the finite-sum derivative bound. amplitude_sum is the definition that computes the L1 norm of the first n terms via (Finset.range n).sum (fun k => |a k|). This sits alongside the Amplitude abbrev from WavefunctionCollapse, which denotes complex quantum amplitudes, though the present bound restricts to real coefficients.
proof idea
Unfold amplitude_sum to expose the Finset sum of absolute values, then apply Finset.sum_nonneg instantiated with the fact that abs_nonneg holds pointwise.
why it matters
Supplies the amplitude_bound field inside the BernsteinCert constructed by bernstein_cert_exists. It directly supports the module goal of proving the finite-sum version of Bernstein's inequality in place of bernstein_inequality_finite_axiom, advancing the structural framework for Recognition Science analysis of bandlimited functions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.