FrequencyBounded
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.
claimA 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 in Recognition Science
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.
scope and limits
- Does not assume any ordering or monotonicity among the frequencies.
- Does not require Ω to be positive.
- Does not extend to infinite sums or continuous spectra.
- Does not itself prove any derivative inequality.
formal statement (Lean)
44def FrequencyBounded (ω : ℕ → ℝ) (n : ℕ) (Ω : ℝ) : Prop :=
proof body
Definition body.
45 ∀ k, k < n → |ω k| ≤ Ω
46