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

7.1 Theorem statements

  • ConvexSubgaussian/GaussianMain.lean: the main theorem file. Defines AdmissibleScale, cStar, and the sharp comparison theorem sharp_convexSubgaussianComparison. Start here.

  • ConvexSubgaussian/GaussianAsymptotics.lean: exposes the explicit constants (\(t_0, A, B, a, p_0, z, c_0\)) and the two named results gaussianDomination_c0 and gaussianSharpness_below_c0.

  • ConvexSubgaussian/CoreDefs.lean: basic definitions: the hinge function, stop-loss transform, and the sub-Gaussian tail condition.

  • ConvexSubgaussian.lean: umbrella import for the package.