poissonConv
plain-language theorem explainer
Poisson convolution at height b of a nonnegative extended-real profile ψ is defined as the Lebesgue convolution of the normalized Poisson kernel with ψ. Researchers building RH certificate windows cite it when constructing the Poisson-plateau function and when proving lower bounds on the infimum c0(ψ). The definition is a direct one-line wrapper that invokes Mathlib's convolution operator on the kernel and profile.
Claim. The Poisson convolution at scale $b$ of a profile $ψ:ℝ→[0,∞]$ is the function $(P_b * ψ)(x)$ obtained by convolving the normalized Poisson kernel $P_b(y)= (1/π) b/(b² + y²)$ with $ψ$ with respect to Lebesgue measure.
background
The CertificateWindow module supplies concrete window functions for the BRF route to the Riemann hypothesis. It defines both a flat-top window scaled by 1/L and a Poisson-plateau window obtained by convolving a profile ψ with the Poisson kernel and scaling. The kernel is the normalized density $P_b(x) = (1/π) b/(b² + x²)$ taking values in extended reals. The convolution appears inside the value set whose infimum defines the manuscript constant c0(ψ) over b ∈ (0,1] and |x| ≤ 1.
proof idea
The definition is a one-line wrapper that applies the Lebesgue convolution operator ⋆ₗ[volume] to the Poisson kernel at parameter b and the input profile ψ.
why it matters
This definition supplies the convolution operation required to build the Poisson-plateau certificate window. It is invoked by lemmas establishing the plateau lower bound c0(ψ) and by the oscillation-control theorem that applies the B1 bridge on Whitney intervals. In the Recognition Science setting it supports the concrete instantiation of the window-to-oscillation implication used in the RH certificate layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.