1 Overview
This blueprint describes the proof of the sharp one-dimensional Gaussian convex comparison theorem: the smallest constant \(c_0\) such that every centered real random variable with two-sided sub-Gaussian tails \(\mathbb {P}(|X|{\gt}t)\le 2e^{-t^2/2}\) is dominated in convex order by \(c_0 G\), where \(G\sim \mathcal N(0,1)\). The constant \(c_0\) is determined by an explicit system of equations and is attained by a canonical extremal distribution that saturates the tail constraint.
Every theorem cited here is formalized in Lean 4 without sorry.
Navigation
Setup and constants: Chapter 2.
Stop-loss route: layer-cake and stop-loss identities, the sharp envelope, and the reduction from stop-loss comparison to convex domination in Chapter 3.
Envelope and extremizer: the construction of the sharp envelope \(J_G\) and of the canonical witness measure \(\mu ^\star \) in Chapter 4.
Gaussian comparator: the closed form for the Gaussian stop-loss transform and the proof that it dominates the envelope at the scale \(c_0\) in Chapter 5.
Module guide: a file-by-file map of the Lean sources in Chapter 7.