Papers With

← All papers
First page of Shifted Anticoncentration for Real Gram Hafnians and Symmetric Gaussian Hafnians

Shifted Anticoncentration for Real Gram Hafnians and Symmetric Gaussian Hafnians

Hongru Zhao

math.PR Sep 6, 2026 · v1 quant-ph
formalization mathlib probability
Read PDF arXiv abstract Code
TL;DR
The main theorems (density bound, shifted anticoncentration, symmetric Gaussian limit) are formalized in Lean 4 with Mathlib, with the proofs published on GitHub.
Abstract
We prove a uniform shifted anticoncentration theorem for the hafnian of a real Gaussian Gram matrix under an explicit condition on the row dimension. After normalization by its root mean square, the law has a bounded continuous density, maximal at zero, and every interval has probability bounded by an explicit coefficient times its radius. Under suitable growth conditions on the row dimension, this coefficient grows at most polynomially in the hafnian order, meaning half the dimension of the Gram matrix. We also compute the exact second moment. The proof exploits the perfect matching structure, combining conditional Gaussian representations, row suspension, and bilinear interpolation to control an inverse moment of the conditional variance. At fixed hafnian order, a rescaled limit as the row dimension grows yields corresponding bounds for the hafnian of a real symmetric Gaussian matrix with independent entries above the diagonal.
Problem

Anticoncentration bounds for hafnians of Gaussian matrices are relevant to hardness arguments for Gaussian boson sampling. Unlike determinants and Pfaffians, hafnians lack orthogonal-invariance reductions to independent product laws, and general bounds for Gaussian polynomials deteriorate with the degree.

Approach

The proof represents the real Gram hafnian conditionally as a Gaussian scale mixture by expanding along a column. It controls the inverse moment of the conditional variance using odd hafnian cofactors, row suspension, an exact bilinear Gaussian interpolation kernel, and a Fourier-to-Laplace comparison recursion. A central limit argument as the row dimension grows transfers the bounds to symmetric Gaussian hafnians. Theorems 2.1 and 2.3 are verified in Lean 4 with Mathlib, with no additional mathematical axioms.

Results

The normalized law has a bounded continuous density that is maximal at zero. Interval probabilities are at most an explicit coefficient times the radius, and this coefficient grows polynomially in n under growth conditions on the row dimension. The exact second moment is (2n-1)!! times the product of (k+2q) for q from 0 to n-1. The Lean proofs are checked by the kernel and pass transitive axiom audits.