bernstein_bound_pos
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.