frequency_bound_nonneg
plain-language theorem explainer
If a sequence of n frequencies satisfies |ω_k| ≤ Ω for every k < n with n positive, then Ω is nonnegative. Analysts replacing Bernstein axioms with formal proofs would cite this to confirm the bandwidth parameter is admissible before deriving derivative bounds. The term proof instantiates the bounding hypothesis at index zero and chains it to the nonnegativity of absolute value via order transitivity.
Claim. Let $ω : ℕ → ℝ$ be a frequency sequence, let $n ∈ ℕ$ with $n > 0$, and let $Ω ∈ ℝ$. If $|ω_k| ≤ Ω$ holds for all $k < n$, then $Ω ≥ 0$.
background
FrequencyBounded is the predicate asserting that every frequency component ω_k with index k less than n lies inside the interval [-Ω, Ω]. The module supplies the finite trigonometric polynomial case of Bernstein's inequality to replace three axioms previously used for bandlimited functions. The imported le_trans supplies transitivity of the order relation on the underlying numeric type.
proof idea
The term proof applies the FrequencyBounded assumption at k = 0 (justified by hn) to obtain |ω 0| ≤ Ω, then composes this with abs_nonneg via le_trans to reach 0 ≤ Ω.
why it matters
The result supplies the elementary nonnegativity check on the bandwidth parameter inside the Bernstein inequality module. It supports the structural framework that replaces the three listed axioms for bandlimited derivative bounds. No downstream declarations are recorded, leaving the lemma as a local sanity condition within the finite-sum development.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.