Papers With

← All papers
First page of A total variation threshold for the first coordinates of uniform parking functions via Lorentzian polynomials

A total variation threshold for the first coordinates of uniform parking functions via Lorentzian polynomials

Igor Kortchemski

math.PR Oct 29, 2026 · v1
formalization autoformalization probability combinatorics
Read PDF arXiv abstract Code
TL;DR
The paper's results were formalized in Lean 4 with Mathlib using AI-assisted autoformalization (Codex) and were checked by Lean's kernel using only standard axioms.
Abstract
Let $π_n$ be a uniform parking function of size $n$. We determine the scale at which its first $k$ coordinates cease to be close in total variation to $k$ independent uniform variables on $\{1,\ldots,n\}$. The distance is comparable to $1\wedge \sqrt{k\log(k+1)/n}$, uniformly for $n\ge2$ and $1\le k\le n$, and tends to one above the scale $n/\log n$. At the critical scale $k\simλn/\log n$, it converges to $2Φ(\sqrt{λ/π})-1$, where $Φ$ is the standard normal distribution function. A key ingredient is the Lorentzian property of the occupation generating polynomial of parking functions. Together with a strengthened Han inequality, this yields a relative entropy estimate for approximation by the product of the one-coordinate marginals.
Problem

How many initial coordinates of a uniform parking function of size n can be observed before its law is distinguishable in total variation from i.i.d. uniform variables on {1,...,n}? The question answers a problem left open by Bellin, who asked whether k_n=o(n) suffices.

Approach

The Lorentzian (strongly log-concave) property of the occupation generating polynomial of parking functions is combined with a strengthened Han inequality. Together these give a relative entropy bound for approximation by the product of the one-coordinate marginals. Total variation between products of those marginals and the uniform product is then estimated using a scalar characterization of product-measure distances. The proofs were developed with substantial assistance from ChatGPT, and an AI-assisted Lean 4 formalization was produced and kernel-checked against the standard axioms of Lean and Mathlib.

Results

The total variation distance is comparable to 1∧sqrt(k log(k+1)/n), uniformly for n≥2 and 1≤k≤n, so the threshold is n/log n rather than n. At the critical scale k λn/log n, the distance converges to 2Φ(sqrt(λ/π))−1.