Prove2Me

Gamma-ratio bound 2k−r−12Γ(k+12)/(Γ(r2)Γ(k−r+1))≤(k+r2)k−r+12/(2Γ(k−r+1))2^{\frac{k-r-1}2}\Gamma(\frac{k+1}2)/(\Gamma(\frac r2)\Gamma(k-r+1))\le(\frac{k+r}2)^{\frac{k-r+1}2}/(2\Gamma(k-r+1))

Proved
GaussianMatrix.tw_gamma_ratio_bound

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

am-gmdeterministicgamma-functiongautschi-inequalitylog-convexityspecial-functions

Let 1≤r≤k1\le r\le k be integers. Then

2(k−r−1)/2 Γ ⁣(k+12)Γ ⁣(r2) Γ(k−r+1)  ≤  12 Γ(k−r+1)(k+r2)(k−r+1)/2,\frac{2^{(k-r-1)/2}\,\Gamma\!\big(\frac{k+1}{2}\big)}{\Gamma\!\big(\frac r2\big)\,\Gamma(k-r+1)}\;\le\;\frac{1}{2\,\Gamma(k-r+1)}\Big(\frac{k+r}{2}\Big)^{(k-r+1)/2},

where Γ\Gamma is Euler's Gamma function.

Equivalently, 2(k−r+1)/2 Γ(k+12)/Γ(r2)≤((k+r)/2)(k−r+1)/22^{(k-r+1)/2}\,\Gamma(\frac{k+1}{2})/\Gamma(\frac r2)\le((k+r)/2)^{(k-r+1)/2}. This is the deterministic step from Tropp–Webber's (B.5) to (B.6): it replaces the density constant of Edelman's bound by an elementary one. The proof writes Γ(k+12)/Γ(r2)=∏i=0k−rΓ(r+i+12)/Γ(r+i2)\Gamma(\frac{k+1}2)/\Gamma(\frac r2)=\prod_{i=0}^{k-r}\Gamma(\frac{r+i+1}{2})/\Gamma(\frac{r+i}{2}), bounds each factor by (r+i)/2\sqrt{(r+i)/2} using Wendel–Gautschi Γ(z+12)≤z1/2Γ(z)\Gamma(z+\frac12)\le z^{1/2}\Gamma(z) (a consequence of log-convexity of Γ\Gamma), and then uses AM–GM in the paired form (r+i)(k−i)≤((k+r)/2)2(r+i)(k-i)\le((k+r)/2)^2 to get ∏i=0k−r(r+i)≤((k+r)/2)k−r+1\prod_{i=0}^{k-r}(r+i)\le((k+r)/2)^{k-r+1}.

Formalization Note. Real.Gamma; the powers are real powers with positive bases. Both sides are positive under the hypotheses.

Preamble
import Definitions.Def_GaussianMatrix_basic

open MeasureTheory ProbabilityTheory
open scoped Matrix
Formal statement
namespace GaussianMatrix

theorem tw_gamma_ratio_bound {r k : ℕ} (hr : 1 ≤ r) (hrk : r ≤ k) :
    2 ^ (((k : ℝ) - r - 1) / 2) * Real.Gamma (((k : ℝ) + 1) / 2)
        / (Real.Gamma ((r : ℝ) / 2) * Real.Gamma ((k : ℝ) - r + 1))
      ≤ (((k : ℝ) + r) / 2) ^ (((k : ℝ) - r + 1) / 2) / (2 * Real.Gamma ((k : ℝ) - r + 1)) := by
  sorry

end GaussianMatrix
Source
J. A. Tropp and R. J. Webber, arXiv:2306.12418, Appendix B, proof of Lemma B.3, the display between (B.5) and (B.6). It uses Γ(z+1/2) ≤ z^{1/2} Γ(z) (J. G. Wendel, Note on the gamma function, Amer. Math. Monthly 55 (1948) 563–564; TW ref. [59]) and (r+i)(k−i) ≤ ((k+r)/2)².

View graph