Papers With

← All papers
First page of Improved Sidorenko bound for hypergraph Turan densities

Improved Sidorenko bound for hypergraph Turan densities

Shuyan Chen, Xinmin Hou, Xizhi Liu

math.CO Oct 13, 2026 · v1
formalization combinatorics
Read PDF arXiv abstract Code
TL;DR
The main Turán density bound, the finite embedding assertion used in its proof, and the existence of the Turán density are formalized in Lean 4.
Abstract
For every fixed integer $r\ge3$, we prove that the Turán density of every $r$-uniform hypergraph $F$ with $m\ge1$ edges satisfies $π(F)\le1-c_rm^{-(r-1)/r}$, where $c_r>0$ depends only on $r$. This improves Sidorenko's general bound, whose gap from $1$ is of order $m^{-1}$. Complete $r$-uniform hypergraphs show that the exponent $(r-1)/r$ is optimal. The proof combines a potential argument for partial embeddings with the Lovász Local Lemma.
Problem

Sidorenko's general upper bound on the Turán density of an r-uniform hypergraph with m edges has a gap from 1 of order 1/m. The question is the optimal order of this gap for fixed r ≥ 3.

Approach

The proof embeds F into a dense host hypergraph in two stages. First, a potential argument assigns vertices with large total conditional failure probability, keeping the chosen host vertices distinct and forming a clique. Second, the remaining vertices are mapped independently, and the Lovász Local Lemma ensures every edge is preserved. The theorem, the finite embedding assertion, and the existence of the Turán density are formalized in Lean 4.

Results

Every r-graph with m edges satisfies π(F) ≤ 1 − c_r m^{-(r-1)/r} with an explicit constant c_r. Complete r-graphs show that the exponent (r−1)/r is optimal, giving 1 − Π_r(m) = Θ_r(m^{-(r-1)/r}).