Theorem 2.2, eq. (1), Hermite-kernel form: $\mathbb E[f(X)g(Y)\,6(P_3-2P_1)]\ge -22/\pi$

Open

GrothendieckConstant.krivine_cubic_kernel_bound

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

functional-analysisharmonic-analysisprobability

Hermite-kernel form of Theorem 2.2, equation (1). Let $(f,g)$ be a Krivine scheme of dimension $k$ : measurable $\pm1$ -valued functions on $\mathbb R^k$ , odd almost everywhere. Let $X,Y$ be independent standard Gaussian vectors in $\mathbb R^k$ and write $s=\langle X,Y\rangle$ . Then

\mathbb E\Big[f(X)\,g(Y)\,\big(s^3-3s\,(|X|^2+|Y|^2)+(3k-6)\,s\big)\Big]\ \ge\ -\frac{22}{\pi}.

Why this is the affine constraint. By Mehler's formula, the density of a $t$ -correlated Gaussian pair divided by the product density is $\sum_n t^n P_n(x,y)$ , with $P_1(x,y)=\langle x,y\rangle$ and

P_3(x,y)=\tfrac16\big(s^3-3s(|x|^2+|y|^2)+3(k+2)s\big),\qquad s=\langle x,y\rangle .

Hence the coefficients of $H(t)=\frac{\pi}{2}\mathbb E[f(X)g(Y_t)]=b_1t+b_3t^3+\cdots$ are $b_1=\frac\pi2\mathbb E[f(X)g(Y)P_1]$ and $b_3=\frac\pi2\mathbb E[f(X)g(Y)P_3]$ , and the integrand above is $6(P_3-2P_1)$ . So the inequality says exactly $\frac{12}{\pi}(b_3-2b_1)\ge-\frac{22}{\pi}$ , i.e. $b_3\ge 2b_1-\frac{11}{6}$ . (The identification of $b_1=H'(0)$ and $b_3=H'''(0)/6$ with these Gaussian integrals, via differentiation under the integral sign, is formally proved in the accompanying reduction of GrothendieckConstant.krivine_scheme_affine_constraint.)

Tightness. For $k=1$ and $f=g=\operatorname{sign}$ (the hyperplane scheme), with $m=\mathbb E|X|=\sqrt{2/\pi}$ and $\mathbb E|X|^3=2m$ , the left side equals $4m^2-12m^2-3m^2=-11m^2=-22/\pi$ , so equality holds.

Formalization note. $\mathbb E$ over independent $X,Y$ is written as the iterated integral against gaussianPairDensity k 0 x y, which is the product of the two standard Gaussian densities.

Preamble

import Mathlib
import Definitions.Def_KrivineSchemeDefs
open MeasureTheory Real

Formal statement

namespace GrothendieckConstant

theorem krivine_cubic_kernel_bound (k : ℕ) (S : KrivineScheme k) :
    -22 / π ≤ ∫ x : Fin k → ℝ, ∫ y : Fin k → ℝ,
      S.f x * S.g y *
        ((∑ i, x i * y i) ^ 3
          - 3 * (∑ i, x i * y i) * (∑ i, x i ^ 2 + ∑ i, y i ^ 2)
          + (3 * (k : ℝ) - 6) * (∑ i, x i * y i)) * gaussianPairDensity k 0 x y := by sorry

end GrothendieckConstant

Source

Li, Saha, Xue, Chaudhuri, Klivans, Kothari, Meka, "Long-Horizon AI Research for Grothendieck Constant: A Case Study in Human-AI Mathematical Collaboration", arXiv:2608.11195v3 (2026), https://arxiv.org/abs/2608.11195, Section 2, p. 6, Theorem 2.2, equation (1): "The correlation function H(t) = b1 t + b3 t^3 + ... of every Krivine scheme satisfies the constraint b3 >= 2 b1 - 11/6." This statement is the equivalent form obtained by expressing b1 and b3 through the degree-1 and degree-3 Mehler (Hermite) kernels; full proof of the constraint in Saha et al., "New upper and lower bounds for the Grothendieck constant" (2026), Part 1.

View graph

Theorem 2.2, eq. (1), Hermite-kernel form: E[f(X)g(Y) 6(P3−2P1)]≥−22/π\mathbb E[f(X)g(Y)\,6(P_3-2P_1)]\ge -22/\piE[f(X)g(Y)6(P3​−2P1​)]≥−22/π

Theorem 2.2, eq. (1), Hermite-kernel form: $\mathbb E[f(X)g(Y)\,6(P_3-2P_1)]\ge -22/\pi$