pith. sign in
module module high

IndisputableMonolith.NumberTheory.RiemannHypothesis.WindowToOscillation

show as:
view Lean formalization →

The window-to-oscillation module defines the Stieltjes function t maps to -w(t) for antitone right-continuous w and supplies lemmas converting such functions into oscillation bounds on intervals. It supports the local-to-global wedge step in the BRF route to the Riemann Hypothesis by enabling measure-theoretic control of essential oscillation. Number theorists working on analytic proofs cite these results for bounding boundary phases after phase rotation. The module assembles auxiliary lemmas on Stieltjes measures rather than a single central証明

claimLet $w$ be antitone and right-continuous. The associated Stieltjes function is $tmapsto -w(t)$, and the module establishes bounds such as the oscillation of $w$ on an interval $I_{cc}$ being controlled by its drop or by a Stieltjes integral over $I_{oo}$ scaled by $pi$.

background

The upstream local-to-global wedge lemma bounds the essential oscillation of a boundary phase $w(t)$ on Whitney or dyadic intervals; after a unimodular rotation this yields the a.e. wedge bound $|w(t)|leq pi cdotUpsilon$. This module introduces the Stieltjes function $t mapsto -w(t)$ built from an antitone right-continuous $w$ to turn window profiles into integral oscillation estimates. It imports Stieltjes measure theory to handle the monotone functions that appear in the window constructions for the RH certificate layer.

proof idea

This module supplies a collection of lemmas that apply Stieltjes measure properties together with antitone monotonicity to bound oscillations on closed intervals, including measure comparisons to integrals and drop estimates. It does not contain one central proof but rather a set of supporting results that implement the wedge lemma in concrete measure language.

why it matters in Recognition Science

The oscillation bounds supplied here feed directly into the downstream CertificateWindow module, which constructs the flat-top and Poisson-plateau windows used in the RH certificate layer. It fills the local-to-global wedge step that appears as a lemma in the Riemann-proofs manuscript, closing the passage from abstract phase control to explicit window estimates.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (7)