FrequencyBounded
plain-language theorem explainer
FrequencyBounded encodes the condition that the first n frequencies in sequence ω lie inside [-Ω, Ω]. Analysts formalizing derivative bounds on trigonometric polynomials cite this predicate when stating the finite-sum case of Bernstein's inequality. The definition is introduced directly as a universal quantification over the initial segment of ω with no auxiliary lemmas.
Claim. A sequence of frequencies $ω : ℕ → ℝ$ is frequency-bounded by $Ω$ up to index $n$ when $|ω(k)| ≤ Ω$ for every $k < n$.
background
The module supplies a Mathlib-native treatment of Bernstein's inequality for finite trigonometric sums, replacing three axioms that would otherwise be assumed for bandlimited functions. FrequencyBounded is the predicate that restricts the frequencies ω_0, …, ω_{n-1} to the interval [-Ω, Ω]. It appears as the hypothesis in the derivative bound for amplitude sums and in the non-negativity result for Ω.
proof idea
The declaration is a direct definition whose body is the predicate ∀ k, k < n → |ω k| ≤ Ω. No tactics or lemmas are invoked; the statement itself is the mathematical content.
why it matters
FrequencyBounded supplies the frequency-support hypothesis inside BernsteinCert and is the key assumption in derivative_bounded_by_frequency, which proves the derivative-amplitude-sum bound. It thereby lets the module discharge the finite-sum version of the Bernstein derivative axiom without external axioms. In the Recognition Science setting this predicate supports controlled frequency content needed for the analytic steps that feed the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.