Prove2Me

Tropp–Webber numerical inequality (B.8): (1+2px+1−2p)Γ(x+2)−2p/(x+1)≤(e/x)2p\big(1+\frac{2p}{x+1-2p}\big)\Gamma(x+2)^{-2p/(x+1)}\le (e/x)^{2p} for 1≤p≤181\le p\le 18, x≥2px\ge 2p

Proved
GaussianMatrix.tw_inverse_moment_numeric

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

gamma-functioninequalitynumerical-boundspecial-functionsstirling

Let pp and xx be natural numbers with 1≤p≤181\le p\le 18 and x≥2px\ge 2p. Then

(1+2px+1−2p)(1Γ(x+2))2p/(x+1)  ≤  (ex)2p.\Big(1+\frac{2p}{x+1-2p}\Big)\Big(\frac{1}{\Gamma(x+2)}\Big)^{2p/(x+1)}\;\le\;\Big(\frac{e}{x}\Big)^{2p}.

Write n=x+1n=x+1 and c=2pc=2p. The inequality is equivalent to (1−c/n)−n/c (n−1)n≤en n!(1-c/n)^{-n/c}\,(n-1)^n\le e^n\,n!. It follows from Stirling's lower bound n!≥2πn (n/e)nn!\ge\sqrt{2\pi n}\,(n/e)^n, the bound (1−1/n)n≤e−1(1-1/n)^n\le e^{-1}, and the concavity of log⁡\log, which gives nlog⁡nn−c≤(c+1)log⁡(c+1)n\log\frac{n}{n-c}\le(c+1)\log(c+1) for n≥c+1n\ge c+1. What remains is the integer check (2p+1)2p+2≤462p≤(2πe2)2p(2p+1)^{2p+2}\le 46^{2p}\le(2\pi e^2)^{2p}, which holds exactly for p≤18p\le 18. This is the last step of the inverse-moment bound E∥(GG⊤)−1∥p≤(e2(k+r)/(2(k−r)2))p\mathbb E\|(GG^\top)^{-1}\|^p\le\big(e^2(k+r)/(2(k-r)^2)\big)^p, applied with x=k−rx=k-r.

Formalization Note. Γ\Gamma is Real.Gamma. The exponent 2p/(x+1)2p/(x+1) is a real power and (e/x)2p(e/x)^{2p} is a natural power. The source states the inequality for real 0≤p≤180\le p\le18 and real x≥2px\ge 2p; here it is specialised to integers p≥1p\ge1 and xx, which is the case used.

Preamble
import Definitions.Def_GaussianMatrix_basic

open MeasureTheory ProbabilityTheory
open scoped Matrix
Formal statement
namespace GaussianMatrix

theorem tw_inverse_moment_numeric {p x : ℕ} (hp : 1 ≤ p) (hp18 : p ≤ 18) (hx : 2 * p ≤ x) :
    (1 + 2 * (p : ℝ) / ((x : ℝ) + 1 - 2 * p))
        * (1 / Real.Gamma ((x : ℝ) + 2)) ^ (2 * (p : ℝ) / ((x : ℝ) + 1))
      ≤ (Real.exp 1 / x) ^ (2 * p) := by sorry

end GaussianMatrix
Source
J. A. Tropp and R. J. Webber, Randomized algorithms for low-rank matrix approximation: design, analysis, and applications, arXiv:2306.12418, Appendix B, proof of Lemma B.3, inequality (B.8) (with the argument (B.9) and Stirling's approximation, Abramowitz–Stegun 6.1.38).

View graph