bernstein_bound_pos
The theorem shows that the derivative bound in a BernsteinBound structure is strictly positive. Analysts replacing axiomatic Bernstein inequalities with explicit constructions for finite trigonometric sums would cite this result when verifying basic sign properties. The proof reduces the bound via its defining equality and applies multiplication positivity to the constants 2, pi and the positive bandwidth.
claimLet $B$ be a structure with positive bandwidth $Omega$ and derivative bound $D$ satisfying $D = 2 pi Omega$. Then $D > 0$.
background
The module supplies a structural framework for Bernstein's inequality, targeting replacement of three axioms with Mathlib proofs and focusing on the finite-sum version for trigonometric polynomials. BernsteinBound is the structure that records a positive real bandwidth together with the equality derivative_bound = 2 * pi * bandwidth. The upstream theorem bandwidth_pos states that recognition bandwidth is positive for positive area, supplying the key positivity hypothesis used here.
proof idea
The proof rewrites the derivative bound using the equality recorded in the BernsteinBound structure. It then applies the mul_pos lemma to the positivity of 2, pi and the bandwidth to conclude that the product is positive.
why it matters in Recognition Science
This result establishes positivity of the derivative bound in the finite trigonometric sum case, directly supporting replacement of the bernstein_inequality_finite_axiom. It contributes to the analysis framework by connecting recognition bandwidth positivity to the derivative bound construction. The declaration forms part of the module's effort to derive Bernstein inequalities constructively rather than axiomatically.
scope and limits
- Does not prove the full Bernstein inequality for general bandlimited functions.
- Does not address the pointwise or far-field zero-free axioms.
- Does not derive explicit numerical bounds beyond the defining relation.
- Does not apply to infinite sums or continuous spectra.
formal statement (Lean)
65theorem bernstein_bound_pos (b : BernsteinBound) : 0 < b.derivative_bound := by
proof body
Term-mode proof.
66 rw [b.bound_eq]
67 exact mul_pos (mul_pos two_pos Real.pi_pos) b.bandwidth_pos
68
69/-! ## Amplitude Bound for Finite Sums
70
71For f(t) = Σ_{k=0}^{n-1} a_k × cos(ω_k × t + φ_k), we have:
72|f(t)| ≤ Σ_k |a_k| (triangle inequality). -/
73