An upper bound for the L¹ Poincaré constant of the Hamming cube

Let C be the smallest constant such that E|f − Ef| ≤ C E|∇f| for every n and every real-valued function f on the Hamming cube {−1,1}n, where |∇f| is the Euclidean length of (D1f, …, Dnf) and Djf(x) = (f(x) − f(x(j)))/2. Ben Efraim and Lust-Piquard proved C ≤ π/2, and the Gaussian case gives C ≥ √(π/2). We prove C = √(π/2), and in dimension n we give an explicit constant cn < √(π/2). By a Pisier-type inequality of Ivanisvili, van Handel and Volberg, it suffices to show that J(λ) ≤ √(π/2) |λ| for every vector λ, where J(λ) = ∫0π/2 E|∑j λjξj| dθ and ξ1, ξ2, … are independent standardized biased random signs that take the positive value with probability (1 + sin θ)/2. For vectors with nonnegative coordinates we compute J exactly, with a mean-value identity for a holomorphic function on the unit disk, and obtain J(λ) < √(π/2) |λ|. For general vectors we prove J(λ) ≤ J(|λ1|, …, |λn|). The main step is that the characteristic function of a centred Bernoulli variable, as a function of the success probability q, equals the characteristic function of an integer-valued random variable at 2πq. The law of this variable is a sampled Fejér kernel. For nonnegative frequencies it is a mixture of laws of a nonnegative integer plus an independent symmetric unimodal variable, so that it and all convolutions of such laws give at least as much mass to k as to −k. We also give an elementary proof of the upper bound, by a transport argument in q. Both bounds, C ≤ √(π/2) and C ≥ √(π/2), are verified in Lean 4 with Mathlib. A computer-assisted proof of the weaker bound C ≤ 1.42 is included as an independent check. The Lean projects, the certificate, the checkers and the programs are archived at doi:10.5281/zenodo.23533351 and available at github.com/tejasvi/hamming-cube-poincare-v2.