Helper lemmas

theorem Rigollet.Chapter1.hasDerivAt_neg_exp_neg_sq_div_two (x : ℝ) : HasDerivAt (fun (x : ℝ) => -Real.exp (-(x ^ 2 / 2))) (x * Real.exp (-(x ^ 2 / 2))) x

The derivative of -exp(-x²/2) is x · exp(-x²/2).

theorem Rigollet.Chapter1.tendsto_neg_exp_neg_sq_div_two : Filter.Tendsto (fun (x : ℝ) => -Real.exp (-(x ^ 2 / 2))) Filter.atTop (nhds 0)

The function -exp(-x²/2) tends to 0 as x → ∞.

theorem Rigollet.Chapter1.integral_Ioi_x_mul_exp (t : ℝ) (ht : 0 < t) : ∫ (x : ℝ) in Set.Ioi t, x * Real.exp (-(x ^ 2 / 2)) = Real.exp (-(t ^ 2 / 2))

The integral of x · exp(-x²/2) over (t, ∞) equals exp(-t²/2) for t > 0. This follows from FTC-2 applied to f(x) = -exp(-x²/2), whose derivative is f'(x) = x · exp(-x²/2).

theorem Rigollet.Chapter1.integrableOn_exp_neg_sq_div_two (t : ℝ) (ht : 0 < t) : MeasureTheory.IntegrableOn (fun (x : ℝ) => Real.exp (-(x ^ 2 / 2))) (Set.Ioi t) MeasureTheory.volume

The function exp(-x²/2) is integrable on (t, ∞) for t > 0.

theorem Rigollet.Chapter1.integrableOn_inv_t_x_mul_exp (t : ℝ) (ht : 0 < t) : MeasureTheory.IntegrableOn (fun (x : ℝ) => t⁻¹ * (x * Real.exp (-(x ^ 2 / 2)))) (Set.Ioi t) MeasureTheory.volume

The function t⁻¹ * x * exp(-x²/2) is integrable on (t, ∞) for t > 0.

Main theorem

theorem Rigollet.Chapter1.proposition_1_1_mills_inequality (t : ℝ) (ht : 0 < t) : ∫ (x : ℝ) in Set.Ioi t, Real.exp (-(x ^ 2 / 2)) ≤ t⁻¹ * Real.exp (-(t ^ 2 / 2))

Goal 0: Mills' inequality (Proposition 1.1 from Rigollet's "High Dimensional Statistics").

For t > 0, the Gaussian tail integral satisfies:

∫_t^∞ exp(-x²/2) dx ≤ (1/t) · exp(-t²/2)

This is the core integral bound underlying Proposition 1.1. The book's statement for general N(μ, σ²) reduces to this by setting μ = 0, σ² = 1.

The proof uses the key observation that for x ≥ t > 0, we have 1 ≤ x/t, so exp(-x²/2) ≤ (x/t) · exp(-x²/2). Integrating both sides and using FTC to evaluate ∫_t^∞ (x/t) exp(-x²/2) dx = (1/t) exp(-t²/2) gives the result.