Gaussian tail analysis: the centered folded normal is 1-sub-Gaussian

This file builds, from scratch against mathlib, the one-dimensional analytic fact underlying the unconditional exponential QJL distortion bound: if Z ~ N(0,1) then the centered folded normal |Z| − √(2/π) is sub-Gaussian with variance proxy 1, i.e.

∀ t, ∫ exp (t · (|Z| − √(2/π))) ≤ exp (t² / 2).

The route is:

• gaussian_foldedMGF: the folded moment generating function in closed form ∫ exp (t·|x|) d(gaussianReal 0 1) = √(2/π) · exp(t²/2) · g t, where g t = ∫ x in Ioi 0, exp (−(x−t)²/2).
• hasDerivAt_g: g is differentiable with g' t = exp(−t²/2) (the parameter sits in the integration limit, so this is the fundamental theorem of calculus, no differentiation under the integral with respect to a fixed domain is needed for the sign analysis).
• two_g_le: the sharp inequality √(2/π) · g t ≤ exp(t·√(2/π)) for all t, proven by a sign analysis of f t = exp(t·√(2/π)) − √(2/π)·g t (f 0 = 0, derivative sign split at 0 and −2√(2/π), with the far-negative tail handled by the trivial bound exp(t·|x|) ≤ 1).
• foldedNormal_subgaussian: assembling the above into HasSubgaussianMGF (|·| − √(2/π)) 1.

noncomputable def JL.gTail (t : ℝ) : ℝ

The "completed-square half-line Gaussian" g t = ∫ x in Ioi 0, exp(−(x−t)²/2).

Equations

• JL.gTail t = ∫ (x : ℝ) in Set.Ioi 0, Real.exp (-(x - t) ^ 2 / 2)

theorem JL.integrable_exp_mul_abs (t : ℝ) : MeasureTheory.Integrable (fun (x : ℝ) => Real.exp (t * |x|)) (ProbabilityTheory.gaussianReal 0 1)

exp (t · |x|) is integrable against the standard Gaussian (dominated by exp (t·x) + exp (−t·x)).

theorem JL.two_mul_inv_sqrt : 2 * (√(2 * Real.pi))⁻¹ = √(2 / Real.pi)

The constant 2·(√(2π))⁻¹ = √(2/π).

theorem JL.gaussian_foldedMGF (t : ℝ) : ∫ (x : ℝ), Real.exp (t * |x|) ∂ProbabilityTheory.gaussianReal 0 1 = √(2 / Real.pi) * Real.exp (t ^ 2 / 2) * gTail t

Folded-normal moment generating function (closed form). For Z ~ N(0,1), ∫ exp(t·|x|) = √(2/π) · exp(t²/2) · g t, where g t = ∫ x in Ioi 0, exp(−(x−t)²/2).

The derivative of gTail

theorem JL.integrable_exp_neg_half_sq : MeasureTheory.Integrable (fun (y : ℝ) => Real.exp (-y ^ 2 / 2)) MeasureTheory.volume

The half-line Gaussian density y ↦ exp(−y²/2) is integrable on ℝ.

theorem JL.integral_exp_neg_half_sq : ∫ (y : ℝ), Real.exp (-y ^ 2 / 2) = √(2 * Real.pi)

The total Gaussian integral ∫ exp(−y²/2) = √(2π).

theorem JL.hasDerivAt_gTail (t : ℝ) : HasDerivAt gTail (Real.exp (-t ^ 2 / 2)) t

Derivative of gTail. g' t = exp(−t²/2). The parameter sits inside the integrand, but a translation x ↦ x − t moves it into the lower integration limit, after which the result follows from the fundamental theorem of calculus for the lower-tail integral s ↦ ∫_{Iic s} exp(−y²/2).

The sharp inequality √(2/π) · gTail t ≤ exp(t · √(2/π))

theorem JL.sqrt_two_div_pi_mul_gTail_zero : √(2 / Real.pi) * gTail 0 = 1

The normalising identity √(2/π) · gTail 0 = 1.

theorem JL.two_g_le (t : ℝ) : √(2 / Real.pi) * gTail t ≤ Real.exp (t * √(2 / Real.pi))

Sharp folded-normal inequality. √(2/π) · gTail t ≤ exp(t · √(2/π)) for all t. This is equivalent to 2·Φ(t) ≤ exp(t·√(2/π)) for the standard normal CDF Φ.

The proof studies f t = exp(t·√(2/π)) − √(2/π)·gTail t, which has f 0 = 0 and derivative f' t = √(2/π)·(exp(t·√(2/π)) − exp(−t²/2)). On [−2√(2/π), ∞) the sign of f' shows 0 is a minimum (isMinOn_Ici_of_deriv), giving f ≥ 0; on the far-negative tail t < −2√(2/π) the bound exp(t·|x|) ≤ 1 yields √(2/π)·gTail t ≤ exp(−t²/2) ≤ exp(t·√(2/π)).

The centered folded normal is 1-sub-Gaussian

theorem JL.foldedNormal_subgaussian : ProbabilityTheory.HasSubgaussianMGF (fun (z : ℝ) => |z| - √(2 / Real.pi)) ⟨1, ⋯⟩ (ProbabilityTheory.gaussianReal 0 1)

The centered folded normal is 1-sub-Gaussian. For Z ~ N(0,1), the centered absolute value |Z| − √(2/π) has a sub-Gaussian moment generating function with variance proxy 1: ∫ exp(t·(|Z| − √(2/π))) ≤ exp(t²/2) for all t.