Standard Gaussian N(0,1) helpers

theorem Rigollet.Chapter1.gaussianPDFReal_zero_one (x : ℝ) : ProbabilityTheory.gaussianPDFReal 0 1 x = (√(2 * Real.pi))⁻¹ * Real.exp (-(x ^ 2 / 2))

The PDF of the standard Gaussian N(0,1) simplifies to (√(2π))⁻¹ · exp(-x²/2).

theorem Rigollet.Chapter1.gaussianReal_Iio_neg_eq_Ioi (t : ℝ) : (ProbabilityTheory.gaussianReal 0 1) (Set.Iio (-t)) = (ProbabilityTheory.gaussianReal 0 1) (Set.Ioi t)

The standard Gaussian N(0,1) is symmetric: P(Z < -t) = P(Z > t).

Standard N(0,1) probability bounds

These are the core results, stated for the standard Gaussian measure gaussianReal 0 1.

theorem Rigollet.Chapter1.proposition_1_1_mills_prob_upper (t : ℝ) (ht : 0 < t) : (ProbabilityTheory.gaussianReal 0 1) (Set.Ioi t) ≤ ENNReal.ofReal ((√(2 * Real.pi))⁻¹ * t⁻¹ * Real.exp (-(t ^ 2 / 2)))

Proposition 1.1, upper tail (standard case). P(Z > t) ≤ (1/(√(2π) · t)) · exp(-t²/2)

theorem Rigollet.Chapter1.proposition_1_1_mills_prob_lower (t : ℝ) (ht : 0 < t) : (ProbabilityTheory.gaussianReal 0 1) (Set.Iio (-t)) ≤ ENNReal.ofReal ((√(2 * Real.pi))⁻¹ * t⁻¹ * Real.exp (-(t ^ 2 / 2)))

Proposition 1.1, lower tail (standard case). P(Z < -t) ≤ (1/(√(2π) · t)) · exp(-t²/2) Follows from symmetry: P(Z < -t) = P(Z > t).

theorem Rigollet.Chapter1.proposition_1_1_mills_prob_abs (t : ℝ) (ht : 0 < t) : (ProbabilityTheory.gaussianReal 0 1) {x : ℝ | t < |x|} ≤ ENNReal.ofReal (2 * (√(2 * Real.pi))⁻¹ * t⁻¹ * Real.exp (-(t ^ 2 / 2)))

Proposition 1.1, absolute value form (standard case). P(|Z| > t) ≤ (2/(√(2π) · t)) · exp(-t²/2) = √(2/π) · exp(-t²/2) / t Follows from the union bound: P(|Z| > t) = P(Z > t) + P(Z < -t) ≤ 2 · P(Z > t).

General Gaussian N(μ, σ²) bounds

The general case follows from the standard N(0,1) case by translation and rescaling. For X N(μ, σ²), we have P(X - μ > t) = P(Z > t/σ) where Z N(0,1). Applying the standard Mills ratio: P(Z > t/σ) ≤ (1/√(2π)) · (σ/t) · exp(-t²/(2σ²))

theorem Rigollet.Chapter1.gaussianReal_shift_Ioi (m : ℝ) (v : NNReal) (s : ℝ) : (ProbabilityTheory.gaussianReal m v) (Set.Ioi (m + s)) = (ProbabilityTheory.gaussianReal 0 v) (Set.Ioi s)

Translation invariance: P_{N(m,v)}(X > m + s) = P_{N(0,v)}(X > s).

theorem Rigollet.Chapter1.gaussianReal_shift_Iio (m : ℝ) (v : NNReal) (s : ℝ) : (ProbabilityTheory.gaussianReal m v) (Set.Iio (m + s)) = (ProbabilityTheory.gaussianReal 0 v) (Set.Iio s)

Translation invariance for lower tail: P_{N(m,v)}(X < m + s) = P_{N(0,v)}(X < s).

theorem Rigollet.Chapter1.gaussianReal_zero_scale_Ioi_div (σ t : ℝ) (hσ : 0 < σ) : (ProbabilityTheory.gaussianReal 0 ⟨σ ^ 2, ⋯⟩) (Set.Ioi t) = (ProbabilityTheory.gaussianReal 0 1) (Set.Ioi (t / σ))

Rescaling (direct form): P_{N(0,σ²)}(X > t) = P_{N(0,1)}(Z > t/σ) for σ > 0.

theorem Rigollet.Chapter1.gaussianReal_zero_Iio_neg (v : NNReal) (s : ℝ) : (ProbabilityTheory.gaussianReal 0 v) (Set.Iio (-s)) = (ProbabilityTheory.gaussianReal 0 v) (Set.Ioi s)

Symmetry of N(0, σ²): P(X < -s) = P(X > s).

theorem Rigollet.Chapter1.proposition_1_1_mills_prob_upper_general (m σ : ℝ) (hσ : 0 < σ) (t : ℝ) (ht : 0 < t) : (ProbabilityTheory.gaussianReal m ⟨σ ^ 2, ⋯⟩) (Set.Ioi (m + t)) ≤ ENNReal.ofReal (σ * (√(2 * Real.pi))⁻¹ * t⁻¹ * Real.exp (-(t ^ 2 / (2 * σ ^ 2))))

Proposition 1.1, upper tail for general N(μ, σ²).

The rescaling proof yields: P(X − m > t) = P(Z > t/σ) ≤ (σ/(t√(2π))) · exp(−t²/(2σ²))

For σ = 1 this matches the book's formula exactly.

theorem Rigollet.Chapter1.proposition_1_1_mills_prob_lower_general (m σ : ℝ) (hσ : 0 < σ) (t : ℝ) (ht : 0 < t) : (ProbabilityTheory.gaussianReal m ⟨σ ^ 2, ⋯⟩) (Set.Iio (m - t)) ≤ ENNReal.ofReal (σ * (√(2 * Real.pi))⁻¹ * t⁻¹ * Real.exp (-(t ^ 2 / (2 * σ ^ 2))))

Proposition 1.1, lower tail for general N(μ, σ²).

By symmetry: P(X − m < −t) ≤ (σ/(t√(2π))) · exp(−t²/(2σ²)).

theorem Rigollet.Chapter1.proposition_1_1_mills_prob_abs_general (m σ : ℝ) (hσ : 0 < σ) (t : ℝ) (ht : 0 < t) : (ProbabilityTheory.gaussianReal m ⟨σ ^ 2, ⋯⟩) {x : ℝ | t < |x - m|} ≤ ENNReal.ofReal (2 * σ * (√(2 * Real.pi))⁻¹ * t⁻¹ * Real.exp (-(t ^ 2 / (2 * σ ^ 2))))

Proposition 1.1, absolute value form for general N(μ, σ²).

Union bound: P(|X − m| > t) ≤ 2σ/(t√(2π)) · exp(−t²/(2σ²)).

Bundled Gaussian tail bound (Proposition 1.1)

The main declaration combining all three parts of the tail bound into a single theorem.

The book (Chapter 1, Section 1.1, Proposition 1.1) states:

P(X − μ > t) ≤ (1/√(2π)) · exp(−t²/(2σ²)) / t P(X − μ < −t) ≤ (1/√(2π)) · exp(−t²/(2σ²)) / t P(|X − μ| > t) ≤ √(2/π) · exp(−t²/(2σ²)) / t

The standard case σ = 1 (which the book primarily proves) matches the formula exactly. For general σ, the book's rescaling argument P(X − μ > t) = P(Z > t/σ) yields the bound with an additional σ factor in the numerator: σ/(t√(2π)) · exp(−t²/(2σ²)). This is an erratum in the book: the stated formula without σ is incorrect for σ > 1 (counterexample: X ~ N(0,4), t = 3 gives P(X > 3) = P(Z > 1.5) ≈ 0.067 but the book's formula gives exp(−9/8)/(3√(2π)) ≈ 0.043).

theorem GaussianTailBound.gaussian_tail_bound_standard (t : ℝ) (ht : t > 0) : (ProbabilityTheory.gaussianReal 0 1) (Set.Ioi t) ≤ ENNReal.ofReal ((√(2 * Real.pi))⁻¹ * t⁻¹ * Real.exp (-(t ^ 2 / 2))) ∧ (ProbabilityTheory.gaussianReal 0 1) (Set.Iio (-t)) ≤ ENNReal.ofReal ((√(2 * Real.pi))⁻¹ * t⁻¹ * Real.exp (-(t ^ 2 / 2))) ∧ (ProbabilityTheory.gaussianReal 0 1) {x : ℝ | t < |x|} ≤ ENNReal.ofReal (2 * (√(2 * Real.pi))⁻¹ * t⁻¹ * Real.exp (-(t ^ 2 / 2)))

Proposition 1.1 (Rigollet, "High Dimensional Statistics"), standard case (σ² = 1).

The book states: Let X be a Gaussian random variable with mean μ and variance σ². Then for any t > 0: P(X − μ > t) ≤ (1/√(2π)) · exp(−t²/(2σ²)) / t P(X − μ < −t) ≤ (1/√(2π)) · exp(−t²/(2σ²)) / t P(|X − μ| > t) ≤ √(2/π) · exp(−t²/(2σ²)) / t

For the standard N(0,1) case (σ = 1), the bound simplifies to: (i) P(Z > t) ≤ 1/(t√(2π)) · exp(−t²/2) (ii) P(Z < −t) ≤ 1/(t√(2π)) · exp(−t²/2) (iii) P(|Z| > t) ≤ 2/(t√(2π)) · exp(−t²/2)

This is the case the book proves directly via Mills' inequality, and the book's stated formula matches exactly when σ = 1.

theorem GaussianTailBound.gaussian_tail_bound (μ σ : ℝ) (hσ : σ > 0) (t : ℝ) (ht : t > 0) : (ProbabilityTheory.gaussianReal μ ⟨σ ^ 2, ⋯⟩) (Set.Ioi (μ + t)) ≤ ENNReal.ofReal (σ * (√(2 * Real.pi))⁻¹ * t⁻¹ * Real.exp (-(t ^ 2 / (2 * σ ^ 2)))) ∧ (ProbabilityTheory.gaussianReal μ ⟨σ ^ 2, ⋯⟩) (Set.Iio (μ - t)) ≤ ENNReal.ofReal (σ * (√(2 * Real.pi))⁻¹ * t⁻¹ * Real.exp (-(t ^ 2 / (2 * σ ^ 2)))) ∧ (ProbabilityTheory.gaussianReal μ ⟨σ ^ 2, ⋯⟩) {x : ℝ | t < |x - μ|} ≤ ENNReal.ofReal (2 * σ * (√(2 * Real.pi))⁻¹ * t⁻¹ * Real.exp (-(t ^ 2 / (2 * σ ^ 2))))

Corollary of Proposition 1.1 for general N(μ, σ²).

For X N(μ, σ²) with σ > 0, the rescaling P(X − μ > t) = P(Z > t/σ) where Z N(0,1) yields the bound with σ in the numerator: (i) P(X − μ > t) ≤ σ/(t√(2π)) · exp(−t²/(2σ²)) (ii) P(X − μ < −t) ≤ σ/(t√(2π)) · exp(−t²/(2σ²)) (iii) P(|X − μ| > t) ≤ 2σ/(t√(2π)) · exp(−t²/(2σ²))

Note: The book's stated formula omits the σ factor. The correct bound from the rescaling argument includes σ (see gaussian_tail_bound_standard for the σ = 1 case that matches the book's formula exactly).