The sharp one-dimensional convex sub-Gaussian comparison constant — Blueprint

7.2 Proof internals

  • ConvexSubgaussian/Internal/GaussianProof.lean: the analytic proof body. Contains the layer-cake lemmas, envelope construction, Gaussian closed-form calculations, monotone ratio argument, construction of the extremal measure, and the reduction from stop-loss comparison to convex domination.