Sharp partition function bound for the attractive logarithmic gas
Matias G. Delgadino, Matthew Rosenzweig, Rishabh Gvalani
math.PR
Nov 11, 2026 · v1
math.AP
TL;DR
The main conditional partition-bound theorem is formalized in Lean as LogGasPaper.main_with_domain, assuming log-HLS, with sources in a public repository.
Abstract
For the attractive logarithmic potential, we prove that the partition function is bounded uniformly in the number of particles on every compact inverse-temperature interval $[0,\be_0]$ with $\be_0<B$, where $B\in(0,2\d]$ is the sharp constant in the logarithmic Hardy–Littlewood–Sobolev inequality. The proof separates a smooth bulk, which inherits the entropy inequality, from a short-range singular interaction. The singular contribution is controlled on the event that each box of a fixed grid contains few particles. The complementary overcrowding event has exponentially small probability, which compensates a crude linear-in-$N$ bound on the log partition function. The resulting estimate supplies the partition bound that can be used recycled in a few different results. A separate Lean formalization verifies the conditional partition-bound theorem under the log-HLS assumption.
Problem
The goal is to bound the partition function of the attractive logarithmic gas on the d-dimensional torus uniformly in the number of particles. The bound should hold for inverse temperatures in any compact interval below the sharp log-HLS constant B.
Approach
The logarithmic kernel is split into a smooth bulk part and a short-range singular part. The bulk inherits the entropy inequality and is controlled by a continuous-kernel entropy–energy bound. The singular part is handled on the event that each grid box has few particles, using an exponential estimate for centered canonical arrays. Overcrowding has exponentially small probability by a Chernoff bound, which offsets a crude linear-in-N bound on the log partition function.
Results
Under the energy-domain hypothesis and the log-HLS inequality, sup over N≥2 and β≤β0 of Z_{N,β} is finite for every β0<B. The conditional theorem is machine-checked in Lean, but the formalization does not prove the log-HLS hypotheses themselves.
