amplitude_sum
plain-language theorem explainer
amplitude_sum defines the L1 norm of the first n coefficients of a real sequence, acting as the amplitude proxy for finite trigonometric polynomials. Analysts formalizing Bernstein bounds for bandlimited functions cite it when deriving nonnegativity and derivative controls. The definition is a direct Finset sum of absolute values over the initial range.
Claim. For a sequence of coefficients $a : ℕ → ℝ$, the amplitude sum up to $n$ is $∑_{k=0}^{n-1} |a(k)|$.
background
The Bernstein Inequality module replaces three axioms with explicit Mathlib proofs for finite trigonometric polynomials of degree n. amplitude_sum supplies the amplitude measure used in the finite-sum version of Bernstein's inequality, where the derivative satisfies ‖f'‖∞ ≤ Ω ‖f‖∞ for frequency bound Ω. Related sibling definitions include FrequencyBounded, which encodes the bandlimit condition on the coefficient sequence, and BernsteinBound, which packages the resulting derivative control.
proof idea
One-line definition that applies Finset.sum to the range 0..n-1 with the absolute-value function.
why it matters
This definition is invoked by amplitude_sum_nonneg, the BernsteinCert structure, and derivative_bounded_by_frequency. It supplies the concrete amplitude term needed to discharge the bernstein_inequality_finite_axiom inside the Recognition Science analysis layer, advancing the finite trigonometric case toward the full bandlimited bound.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.