Sidorenko's conjecture (1993)

The question

sidorenko_conjecture. Sidorenko's conjecture (1993).

For every finite bipartite simple graph $H$ and every finite simple graph $G$: $t(H,G)\ge t(K_2,G{)}^{e(H)}$, where $K_2$ denotes the single-edge graph on 2 vertices (i.e. completeGraph (Fin 2)).

sidorenko_conjecture_graphon. Sidorenko's conjecture for graphons (1993).

For every finite bipartite simple graph $H$ and every graphon $W$ on $[0,1]$ with Lebesgue measure: $t(H,W)\ge t(K_2,W{)}^{e(H)}$, where $t(K_2,W)=p(W)$ is the edge density of $W$, and $t(H,W)$ is the graphon homomorphism density of $H$ in $W$.

tournament_anti_sidorenko_trees_conjecture. Tournament Anti-Sidorenko (TAS) Trees Conjecture.

For every finite undirected tree $T$, there exists an orientation $\vec{T}$ of its edges such that for any finite tournament $G$, the homomorphism density satisfies: $$t_{\vec{T}}(G)\le 2^{-e(T)}$$ where $e(T)$ is the total number of edges in $T$.

tournament_anti_sidorenko_trees_conjecture_tournamenton. Tournament Anti-Sidorenko (TAS) Trees Conjecture (Tournamenton limit version).

For every finite undirected tree $T$, there exists an orientation $\vec{T}$ of its edges such that for every tournamenton $W:[0,1{]}^2\to [0,1]$, the homomorphism density satisfies: $$t_{\vec{T}}(W)\le 2^{-e(T)}$$ where $e(T)$ is the total number of edges in $T$.

Formal statement (Lean 4)

From Formal Conjectures, module FormalConjectures.Wikipedia.SidorenkoConjecture (4 statements). answer(sorry) marks a yes/no question: a proof of the statement on the right of ↔, or of its negation, answers it.

theorem sidorenko_conjecture : answer(sorry) ↔
    ∀ {V W : Type} [Fintype V] [Fintype W] [DecidableEq V] [DecidableEq W] [Nonempty W]
      (H : SimpleGraph V) (G : SimpleGraph W)
      [DecidableRel H.Adj] [DecidableRel G.Adj],
      H.IsBipartite →
      homDensity (completeGraph (Fin 2)) G ^ H.edgeFinset.card ≤ homDensity H G

theorem sidorenko_conjecture_graphon : answer(sorry) ↔
    ∀ {V : Type*} [Fintype V] [DecidableEq V] (H : SimpleGraph V) [DecidableRel H.Adj],
      H.IsBipartite →
      ∀ (W : Graphon),
        (graphonEdgeDensity W) ^ H.edgeFinset.card ≤ graphonHomDensity H W

theorem tournament_anti_sidorenko_trees_conjecture : answer(sorry) ↔
    ∀ {V : Type*} [Fintype V] [DecidableEq V] (T : SimpleGraph V) [DecidableRel T.Adj],
      T.IsTree →
      ∃ (D : Digraph V),
        D.IsOrientation T ∧
        ∀ {W : Type*} [Fintype W] [DecidableEq W] [Nonempty W]
          (G : Digraph W) [DecidableRel G.Adj],
          G.IsTournament →
          Digraph.homDensity D G ≤ (1 / 2 : ℝ) ^ T.edgeFinset.card

theorem tournament_anti_sidorenko_trees_conjecture_tournamenton : answer(sorry) ↔
    ∀ {V : Type*} [Fintype V] [DecidableEq V] (T : SimpleGraph V) [DecidableRel T.Adj],
      T.IsTree →
      ∃ (D : Digraph V),
        D.IsOrientation T ∧
        ∀ (W : LimitObjects.Tournamenton),
          tournamentonHomDensity D W ≤ (1 / 2 : ℝ) ^ T.edgeFinset.card

What counts as progress

• A Lean proof of one of the statements above, pinned as the claim's formal statement.
• Partial results: special cases, weaker bounds, reductions — as verified claims.
• Computations and numerical evidence with published code (reproducible).
• Literature: the problem may have been solved or partly solved already. Report it as a literature claim.
• A precise flaw in the formal statement (a misformalisation) — report it upstream too.

References

• Wikipedia
• [Si93] Sidorenko, A. (1993). "A correlation inequality for bipartite graphs." Graphs Combin. 9, pp. 201--204.
• [CoFo10] Conlon, D. and Fox, J. (2010). "Bounds for graph regularity and removal lemmas." Geom. Funct. Anal. 22, pp. 1191--1256.
• [KLL18] Kim, J.H., Lee, C., Lee, J. (2018). "Two approaches to Sidorenko's conjecture." Trans. Amer. Math. Soc. 370, pp. 8515--8552.
• [ArXiv2605] arXiv:2605.14138
• [BR65] Blakley, G. R. and Roy, P. (1965). "A Hölder type inequality for symmetric matrices with nonnegative entries." Proc. Amer. Math. Soc. 16, pp. 1244--1245.

Source and licence

Imported from Formal Conjectures (Wikipedia), commit e6d1743831c2. Statements and descriptions © The Formal Conjectures Authors, Apache License 2.0; reformatted for this page.