Chi-squared moment generating function and concentration

Building on sqGaussian_mgf, this file constructs the sum of k i.i.d. squared standard Gaussians as the coordinate sum under the product measure gaussianVec k = Measure.pi (fun _ : Fin k => stdGaussian), computes its moment generating function

mgf (chiSq k) (gaussianVec k) t = ((1 - 2t)^(-1/2))^k,

and derives two-sided chi-squared tail bounds via mathlib's Chernoff bound, optimised at the Dasgupta–Gupta choice of t:

• upper: P(S ≥ (1+ε)k) ≤ exp(-(ε² - ε³) k / 4),
• lower: P(S ≤ (1-ε)k) ≤ exp(-(ε² - ε³) k / 4).

The analytic crux is reduced to two scalar logarithmic inequalities, proven by the monotonicity of an explicit auxiliary function.

Scalar logarithmic inequalities

theorem JL.log_one_add_le {ε : ℝ} (hε : 0 ≤ ε) : Real.log (1 + ε) ≤ ε - ε ^ 2 / 2 + ε ^ 3 / 2

log (1 + ε) ≤ ε - ε²/2 + ε³/2 for ε ≥ 0.

theorem JL.log_one_sub_le {ε : ℝ} (hε : 0 ≤ ε) (hε1 : ε < 1) : Real.log (1 - ε) ≤ -ε - ε ^ 2 / 2 + ε ^ 3 / 2

log (1 - ε) ≤ -ε - ε²/2 + ε³/2 for 0 ≤ ε < 1.

theorem JL.scalar_upper {ε : ℝ} (h0 : 0 < ε) : Real.exp (-(ε / 2)) * √(1 + ε) ≤ Real.exp (-(ε ^ 2 - ε ^ 3) / 4)

The base scalar inequality controlling the upper chi-squared tail.

theorem JL.scalar_lower {ε : ℝ} (h0 : 0 < ε) (h1 : ε < 1) : Real.exp (ε / 2) * √(1 - ε) ≤ Real.exp (-(ε ^ 2 - ε ^ 3) / 4)

The base scalar inequality controlling the lower chi-squared tail.

The chi-squared random variable and its MGF

noncomputable def JL.gaussianVec (k : ℕ) : MeasureTheory.Measure (Fin k → ℝ)

The product Gaussian measure on Fin k → ℝ: k i.i.d. N(0,1) coordinates.

Equations

• JL.gaussianVec k = MeasureTheory.Measure.pi fun (x : Fin k) => JL.stdGaussian

instance JL.instIsProbabilityMeasureForallFinRealGaussianVec (k : ℕ) : MeasureTheory.IsProbabilityMeasure (gaussianVec k)

noncomputable def JL.chiSq (k : ℕ) : (Fin k → ℝ) → ℝ

The chi-squared random variable with k degrees of freedom: the sum of the squared coordinates.

Equations

• JL.chiSq k ω = ∑ i : Fin k, ω i ^ 2

theorem JL.chiSq_mgf (k : ℕ) {t : ℝ} (ht : t < 1 / 2) : ProbabilityTheory.mgf (chiSq k) (gaussianVec k) t = (√(1 - 2 * t))⁻¹ ^ k

Chi-squared MGF. For t < 1/2, E[exp (t · S)] = ((1 - 2t)^(-1/2))^k.

theorem JL.integrable_exp_mul_sq {t : ℝ} (ht : t < 1 / 2) : MeasureTheory.Integrable (fun (x : ℝ) => Real.exp (t * x ^ 2)) stdGaussian

Integrability of exp (t · Z²) against N(0,1) for t < 1/2.

theorem JL.integrable_exp_mul_chiSq (k : ℕ) {t : ℝ} (ht : t < 1 / 2) : MeasureTheory.Integrable (fun (ω : Fin k → ℝ) => Real.exp (t * chiSq k ω)) (gaussianVec k)

Integrability of exp (t · S) for t < 1/2.

Two-sided chi-squared tail bounds

theorem JL.chiSq_upper_tail (k : ℕ) {ε : ℝ} (h0 : 0 < ε) : (gaussianVec k).real {ω : Fin k → ℝ | (1 + ε) * ↑k ≤ chiSq k ω} ≤ Real.exp (-(ε ^ 2 - ε ^ 3) * ↑k / 4)

Upper chi-squared tail. P(S ≥ (1+ε)k) ≤ exp(-(ε² - ε³) k / 4).

theorem JL.chiSq_lower_tail (k : ℕ) {ε : ℝ} (h0 : 0 < ε) (h1 : ε < 1) : (gaussianVec k).real {ω : Fin k → ℝ | chiSq k ω ≤ (1 - ε) * ↑k} ≤ Real.exp (-(ε ^ 2 - ε ^ 3) * ↑k / 4)

Lower chi-squared tail. P(S ≤ (1-ε)k) ≤ exp(-(ε² - ε³) k / 4).