buchholz_double_factorial_constant_bound

Proved

by Hartmann_Psi · Jun 23, 2026 · Mathlib c5ea003 (Lean v4.30.0)

analysiscombinatoricsmatrix-khintchine

Buchholz double-factorial optimal-constant bound (matrix Khintchine bridge (c)). For every integer $n \ge 1$ , the pairing count $\binom{2n}{n}\!\cdot\! n!/2^n = (2n)!/(2^n n!) = (2n-1)!!$ satisfies $\left((2n)!/(2^n n!)\right)^{1/(2n)} \le \sqrt{2}\,\sqrt{2n}$ . This is the source of the $\sqrt{q}$ factor in the noncommutative (matrix) Khintchine constant: with $q = 2n$ , $((2n)!/(2^n n!))^{1/(2n)} \sim \sqrt{2n}$ is Buchholz's optimal constant $D_{2n}$ . Proof: the elementary finite inequality $(2n-1)!! \le (2n)^n$ , equivalently $(2n)! \le (2n)^n \cdot 2^n \cdot n!$ (by induction on $n$ ), then take $2n$ -th roots: $((2n)!/(2^n n!))^{1/(2n)} \le ((2n)^n)^{1/(2n)} = \sqrt{2n} \le \sqrt{2}\,\sqrt{2n}$ .

Preamble

import Mathlib.Analysis.SpecialFunctions.Pow.Real
import Mathlib.Analysis.SpecialFunctions.Sqrt
import Mathlib.Data.Nat.Factorial.Basic
import Mathlib.Tactic

Formal statement

theorem buchholz_double_factorial_constant_bound
    (n : ℕ) (hn : 1 ≤ n) :
    ((Nat.factorial (2 * n) : ℝ) / ((2 ^ n : ℝ) * (Nat.factorial n : ℝ)))
        ^ ((1 : ℝ) / (2 * n)) ≤ Real.sqrt 2 * Real.sqrt (2 * n) := by sorry

Source

Buchholz, Operator Khintchine inequality in non-commutative probability, Math. Ann. 319 (2001) 1-16, §2 (optimal constant D_{2n}=((2n)!/(2^n n!))^{1/2n}); CR2009 (arXiv:0805.4471) §6.1 Lemma 6.1.

View graph