oscOn_Icc_whitney_le_mul_L_of_flatTop
plain-language theorem explainer
Analysts working on the Riemann Hypothesis via BRF certificates cite this to bound the essential oscillation of an antitone w on the closed interval of length 2L centered at t0 by D L. The hypothesis requires that the Stieltjes integral of the flat-top window (scaled by 1/L with ψ equal to 1 on the unit interval) against the measure of -w is at most D. The proof first confirms the lower bound 1/L on the open interval via the plateau lemma, applies the general window-to-oscillation bridge, and simplifies the resulting quotient to the product via
Claim. Let w be antitone and right-continuous. Let ψ satisfy ψ(x)=1 for |x|≤1. For L>0, D≥0 and t₀∈ℝ, if the integral of the flat-top window φ_{L,t₀}(t) := ψ((t-t₀)/L)/L (lifted to the extended reals) against the Stieltjes measure induced by -w is ≤D, then the essential oscillation of w on the closed interval [t₀-L,t₀+L] is at most DL.
background
The module builds explicit certificate windows for the BRF route to the Riemann Hypothesis. The flat-top window is defined by φ_{L,t₀}(t) = ENNReal.ofReal(ψ((t-t₀)/L)/L). The essential oscillation oscOn w s is the difference between essential supremum and infimum of w over s with respect to Lebesgue measure. The Stieltjes measure stieltjesNeg.μ is generated by the antitone right-continuous function t↦-w(t).
proof idea
The argument first verifies t₀-L < t₀+L by linear arithmetic and positivity of 1/L. It applies the plateau lemma lower_of_plateau_one to obtain ENNReal.ofReal(1/L) ≤ flat-top window on the open interval. It then invokes the general bridge oscOn_Icc_le_div_of_window_lintegral_bound with c=1/L to conclude oscOn ≤ D/(1/L). The final step uses le_trans together with field_simp to replace the quotient by the product DL.
why it matters
This supplies the concrete flat-top case of the B1 window-to-oscillation bridge in the RH certificate layer. It directly converts an integral bound on the scaled plateau window into an oscillation bound scaled by L, supporting the control of oscillations required in the Recognition Science number-theory route. No downstream uses are recorded, indicating its role as an intermediate building block.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.