The Sharp One-Dimensional Convex Sub-Gaussian Comparison Constant

Damek Davis and Sam Power

A Lean 4 formalization of the sharp one-dimensional Gaussian convex comparison theorem: the optimal constant c0 such that every centered sub-Gaussian random variable is dominated in convex order by c0 G, where G is standard normal.