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

7.3 Suggested reading order

  1. GaussianMain.lean for the theorem statement.

  2. GaussianAsymptotics.lean for the explicit constants and the domination/sharpness split.

  3. This blueprint to navigate the proof in Internal/GaussianProof.lean.