BernsteinCert
plain-language theorem explainer
BernsteinCert packages the nonnegativity of the amplitude sum together with the derivative bound under a frequency constraint for finite sequences. Analysts replacing axiomatic Bernstein assumptions with explicit finite-sum constructions would cite this structure when building certificates. The declaration is a direct record definition that encodes the two inequalities as fields.
Claim. A structure consists of two properties: for all sequences $a$ and integers $n$, the sum $S(a,n) = 0$ where $S(a,n) = 0$ is the sum of absolute values; and for all sequences $a$, $ω$, integers $n$, and $Ω ≥ 0$, if $|ω_k| ≤ Ω$ for all $k < n$, then the weighted sum $∑ |a_k ω_k| ≤ Ω ⋅ sum |a_k|.
background
The module supplies a structural framework for Bernstein's inequality in the finite trigonometric polynomial case, with the goal of replacing three axioms (pointwise bound, finite-sum derivative bound, and far-field zero-free region) by direct proofs. Amplitude sum is the sum of absolute values over the first n terms. Derivative amplitude sum is the corresponding sum weighted by the frequencies. FrequencyBounded is the predicate that each frequency satisfies |ω_k| ≤ Ω for k < n.
proof idea
The declaration is a structure definition with no proof body. It directly specifies the two field predicates by referencing amplitude_sum, derivative_amplitude_sum, and the FrequencyBounded predicate.
why it matters
This structure supplies the certificate used by the downstream theorem bernstein_cert_exists to witness Nonempty BernsteinCert via amplitude_sum_nonneg and derivative_bounded_by_frequency. It advances the module's replacement of the finite-sum Bernstein axiom. In the Recognition Science setting the bound supports analytic steps that appear in zero-free region arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.