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

5.2 The tail region \(u \ge a\)

Lemma 14 Monotone-ratio argument
✓
#

Lean declarations

The ratio

\[ R(u) := \frac{\overline{\Phi }(u/c_0)}{2e^{-u^2/2}} \]

is increasing on \([a,\infty )\), and the corresponding monotone-ratio principle converts this monotonicity into a comparison between the Gaussian stop-loss and the tail-integral branch of the envelope.

Proof ▶

The derivative of \(\log R\) is controlled using Mills-ratio bounds for the Gaussian tail. The monotone-ratio principle then converts the sign of the derivative into a monotonicity statement for the difference of two functions that share the same limit at infinity.

Theorem 15 Gaussian stop-loss dominates the envelope
✓
#

Uses

Lean declarations

For every \(u \ge 0\),

\[ g_{c_0}(u) \ge J_G(u). \]
Proof ▶

On \([0,a]\), the envelope equals the affine function \(B-p_0u\), so Lemma 13 gives the inequality directly. For \(u \ge a\), the envelope is the tail integral \(\int _u^\infty s_G(t)\, dt\). The difference between the Gaussian stop-loss and that tail integral is nonnegative at \(u=a\) (from the affine-contact inequality) and tends to \(0\) at infinity. The monotone-ratio argument (Lemma 14) forces the difference to stay nonnegative on the entire interval \([a,\infty )\).