bernstein_cert_exists
plain-language theorem explainer
The theorem asserts existence of a BernsteinCert by direct construction from two supporting results on amplitude sums. Researchers replacing axiomatic bounds in bandlimited analysis with explicit proofs would cite it for the finite trigonometric case. The proof is a term-mode instantiation that populates the structure fields with the nonnegativity lemma and the frequency-derivative bound lemma.
Claim. There exists a certificate structure such that for every sequence of real amplitudes and every finite degree the total amplitude sum is nonnegative, and for every frequency sequence, degree, and cutoff frequency at least zero satisfying the frequency-boundedness condition the derivative amplitude sum is at most the cutoff times the amplitude sum.
background
BernsteinCert is the structure whose two fields encode the required nonnegativity of amplitude sums and the derivative bound under frequency constraints. amplitude_sum is the sum of absolute values over the first n terms; derivative_amplitude_sum is the corresponding weighted sum that appears after differentiation of the trigonometric polynomial. FrequencyBounded is the hypothesis that all frequencies lie inside the cutoff interval of width Omega. The module replaces three Bernstein axioms with Mathlib proofs for the finite-sum version, as stated in the module header.
proof idea
The proof is a one-line term construction that builds the structure by assigning the amplitude_bound field to the theorem amplitude_sum_nonneg and the derivative_bound field to the theorem derivative_bounded_by_frequency.
why it matters
The declaration supplies the concrete certificate needed to discharge the finite trigonometric case inside the Bernstein inequality module. It directly supports the module's aim of replacing the three listed axioms with explicit proofs, thereby closing the structural gap for bandlimited derivative estimates in the Recognition Science analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.