Prove2Me

LqL^q norm of a reciprocal chi-square: E[Ξ−q]<(3/d)q\mathbb{E}[\Xi^{-q}] < (3/d)^q for q=(d−1)/2q=(d-1)/2, d≥5d \ge 5 (HMT Lemma A.10)

Proved
GaussianMatrix.inv_chi_square_Lq_bound

by tc · Oct 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

chi-squaregamma-functionlq-normmomentsprobability

Let d≥5d \ge 5 and let Ξ=∑j=1dxj2\Xi = \sum_{j=1}^d x_j^2 with x∼N(0,Id)x \sim \mathcal{N}(0, I_d), a chi-square variable with dd degrees of freedom. Put q=(d−1)/2q = (d-1)/2. Then Ξ−q\Xi^{-q} is integrable and

E[Ξ−q]  <  (3d)q,i.e.Eq(Ξ−1)=(E Ξ−q)1/q<3d.\mathbb{E}\big[\Xi^{-q}\big] \;<\; \Big(\frac{3}{d}\Big)^{q}, \qquad\text{i.e.}\qquad \mathbb{E}_q\big(\Xi^{-1}\big) = \big(\mathbb{E}\,\Xi^{-q}\big)^{1/q} < \frac{3}{d}.

By the negative-moment formula, E[Ξ−q]=Γ(1/2)/(2qΓ(d/2))=π/(2qΓ(d/2))\mathbb{E}[\Xi^{-q}] = \Gamma(1/2)/(2^q\Gamma(d/2)) = \sqrt{\pi}/(2^q\Gamma(d/2)), so the claim is the Gamma-function inequality π d q<6q Γ(d/2)\sqrt{\pi}\, d^{\,q} < 6^{q}\,\Gamma(d/2).

This is the key moment estimate in the tail bound for ∥G†∥F2\|G^\dagger\|_F^2: each diagonal entry of (GG⊤)−1(GG^\top)^{-1} for an r×kr\times k Gaussian GG is distributed as 1/χk−r+121/\chi^2_{k-r+1}, and the bound with d=k−r+1d = k-r+1 and q=(k−r)/2q = (k-r)/2 controls its LqL^q norm.

Formalization Note. The power is the real power Real.rpow applied to the nonnegative quantity (∑jxj2)−1(\sum_j x_j^2)^{-1} (with 0−1=00^{-1}=0). HMT state the lemma for 2≤q≤(d−1)/22 \le q \le (d-1)/2 and reduce it to the endpoint q=(d−1)/2q=(d-1)/2 by Hölder's inequality; only the endpoint case is formalized here.

Preamble
import Definitions.Def_GaussianMatrix_basic

open MeasureTheory ProbabilityTheory
open scoped Matrix
Formal statement
namespace GaussianMatrix

theorem inv_chi_square_Lq_bound {d : ℕ} (hd : 5 ≤ d) :
    Integrable (fun x : Fin d → ℝ => ((∑ j, x j ^ 2)⁻¹) ^ (((d : ℝ) - 1) / 2))
        (Measure.pi fun _ : Fin d => gaussianReal 0 1) ∧
    ∫ x, ((∑ j, x j ^ 2)⁻¹) ^ (((d : ℝ) - 1) / 2) ∂(Measure.pi fun _ : Fin d => gaussianReal 0 1)
      < (3 / (d : ℝ)) ^ (((d : ℝ) - 1) / 2) := by sorry

end GaussianMatrix
Source
N. Halko, P.-G. Martinsson, J. A. Tropp, Finding structure with randomness: Probabilistic algorithms for constructing approximate matrix decompositions, SIAM Review 53(2) (2011), 217–288 (arXiv:0909.4061), Lemma A.10 (arXiv version p. 67): for k≥5k \ge 5 and 2≤q≤(k−1)/22 \le q \le (k-1)/2, Eq(Ξ−1)<3/k\mathbb{E}_q(\Xi^{-1}) < 3/k; the proof there establishes exactly the endpoint case q=(k−1)/2q = (k-1)/2 stated here.

View graph