The sharp one-dimensional convex sub-Gaussian comparison constant — Blueprint
1
Overview
▶
Navigation
2
Setup and constants
▶
2.1
The comparison problem
2.2
Comparison and sharpness statements
3
Stop-loss route
▶
3.1
Layer-cake and stop-loss identities
3.2
The sharp stop-loss envelope
3.3
From stop-loss control to convex domination
4
Envelope and extremizer
▶
4.1
The envelope parameters
4.2
The canonical extremal measure
5
Gaussian comparator
▶
5.1
Closed form and tangent point
5.2
The tail region \(u \ge a\)
6
Main theorem
7
Module guide
▼
7.1
Theorem statements
7.2
Proof internals
7.3
Suggested reading order
Dependency graph
7 Module guide
This chapter records the role of each Lean file.
7.1
Theorem statements
7.2
Proof internals
7.3
Suggested reading order