derivative_bounded_by_frequency
plain-language theorem explainer
Analysts replacing axiomatic Bernstein bounds with explicit proofs cite this result for finite trigonometric sums. It shows that if each frequency satisfies |ω_k| ≤ Ω then the summed absolute derivative is at most Ω times the summed absolute amplitude. The argument unfolds the two sums and applies the componentwise bound from FrequencyBounded together with nonnegativity.
Claim. Let $a,ω:ℕ→ℝ$, $n∈ℕ$, and $Ω∈ℝ$ with $Ω≥0$. If $|ω(k)|≤Ω$ for all $k<n$, then $∑_{k=0}^{n-1}|a(k)⋅ω(k)|≤Ω⋅∑_{k=0}^{n-1}|a(k)|$.
background
amplitude_sum computes the total variation of the coefficient vector a over the first n indices. derivative_amplitude_sum does the same but weights each term by its frequency ω_k. FrequencyBounded encodes the bandlimit condition that no frequency exceeds Ω in absolute value. This module replaces the Bernstein axioms for finite sums with direct Mathlib proofs. The setting is the finite trigonometric polynomial case of Bernstein's inequality, where the derivative bound follows from the frequency constraint without invoking the full bandlimited theory.
proof idea
The proof unfolds both sums, rewrites the right-hand side as a sum, then applies Finset.sum_le_sum. For each index it uses the absolute value of the product and multiplies the frequency bound by the nonnegative absolute amplitude.
why it matters
This theorem supplies the derivative bound component of the BernsteinCert constructed in bernstein_cert_exists. It directly addresses the finite-sum version of Bernstein's inequality listed in the module documentation as one of the axioms to replace. In the Recognition Science framework it supports the structural replacement of the bandlimited derivative bound axiom for the finite case.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.