TejasviTomar
October 2026 · Preprint

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

Tejasvi Singh Tomar

In plain words

Poincaré inequalities bound how far a function strays, on average, from its mean by a constant times the average size of its changes. On the Hamming cube, the strings of n plus and minus signs on which Boolean functions live, the best constant C is unknown. Ben Efraim and Lust-Piquard proved that C is at most π/2, about 1.5708, and later work lowered this by 0.00013. The Gaussian case shows that C is at least 1.2533. The new bound is C ≤ 1.42 in every dimension, with a proof also checked in the Lean proof assistant.

Abstract

Let C be the smallest constant such that E|f − Ef| ≤ C E|∇f| for every n and every real 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. Ivanisvili, Li, van Handel and Volberg showed C < π/2, and Ivanisvili and Stone obtained C ≤ π/2 − 1.3·10−4. The Gaussian case gives C ≥ √(π/2). We prove C ≤ 1.42. By a Pisier-type inequality of Ivanisvili, van Handel and Volberg, E|f − Ef| is at most the average over the cube of J(∇f), 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. Hence C ≤ K, the supremum of J over unit vectors. Bounding the integrand separately for each θ, as earlier arguments do, cannot give less than 1.4217. We bound E|∑j λjξj| by E h(∑j λjξj) for even polynomials h ≥ |·| of degree six. The bound depends on λ only through ∑λj3, ∑λj4 and ∑λj6, so it does not depend on the dimension. A certificate with 1761 polynomials, 302 squares in the plane of (∑λj4, ∑λj6) and 1024 intervals of θ is verified in exact rational and ball arithmetic. We also show that J(λ) < √(π/2) |λ| when all λj have the same sign, while K ≥ √(π/2). Thus C = √(π/2) would follow from the inequality J(λ) ≤ J(|λ1|, …, |λn|). The bound C ≤ 1.42 and the bound K ≤ 1.42 are also verified in Lean 4 with Mathlib, by the Lean kernel and with the standard axioms only.

Left: a triangle pointing right, outlined in teal and filled with a mosaic of vertical strips and slanted wedge-shaped tiles in shades of pink, medium pink on the left, darkest around the middle near the upper edge, and fading to almost white towards the tip, with a small yellow mark on the upper edge, just right of the middle. Right: a black V shape with a fan of thin curves, teal to yellow, that hug it from above, touching its arms and rounding off above the point of the V.
Illustration of the certificate. Left: the region R = {P₄² ≤ P₆ ≤ P₄^(3/2)}, which contains every possible pair (P₄, P₆) = (Σλⱼ⁴, Σλⱼ⁶) for unit vectors λ, on logarithmic scales: log₂ P₄ runs across, from −12 at the left edge to 0 at the tip, and log₂ P₆ − 1.75 log₂ P₄ runs up, so that the edges P₆ = P₄^(3/2) (top) and P₆ = P₄² (bottom) become the two equal sides of a triangle. Each tile is the part of R in one of the 302 leaf squares of the certificate, shaded on a logarithmic scale by its slack, the amount by which the certificate's bound on that square, a sum over 1024 intervals of θ, stays below 71/50 = 1.42 (darker magenta where the slack is smaller); the yellow outline marks the square with the smallest slack, about 0.0018. The paper's two checking programs compute rigorous but looser bounds, whose largest values, 1.4198937 and 1.4184488, fall on other squares. Right: |z| in black, and the even polynomials h(z) = a + bz² + cz⁴ + dz⁶ ≥ |z| that the certificate uses on that square for every eighth interval of θ, 128 of the 1024, with only 31 different polynomials among them, so many curves overlap; they are coloured from teal (θ near 0) to yellow (θ near π/2). Because h ≥ |z|, E|S| ≤ E h(S) = a + b + c·ES⁴ + d·ES⁶ for S = Σⱼλⱼξⱼ, where the ξⱼ are independent random signs, positive with probability (1 + sin θ)/2, shifted and scaled to mean 0 and variance 1, so that ES² = 1. The picture is computed in floating point from the certificate's exact data.