1. FormalConjectures
  2. Wikipedia
  3. SidorenkoConjecture
/- Copyright 2026 The Formal Conjectures Authors. Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License. You may obtain a copy of the License at https://www.apache.org/licenses/LICENSE-2.0 Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License. -/ import FormalConjecturesUtil

Sidorenko's conjecture (1993)

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.

open Finset SimpleGraphnamespace SidorenkoConjectureopen LimitObjects/- ## Homomorphism density We use `SimpleGraph.homCount` / `SimpleGraph.homDensity` from `FormalConjecturesForMathlib.Combinatorics.SimpleGraph.HomDensity` for finite host graphs, and `graphonHomDensity` / `graphonEdgeDensity` from `FormalConjecturesForMathlib.Combinatorics.LimitObjects.Graphon` for graphons on measure spaces. -/ variable {V W : Type*}

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)).

@[category research open, AMS 5] 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 := ⊢ True ↔ ∀ {V W : Type} [inst : Fintype V] [inst_1 : Fintype W] [inst_2 : DecidableEq V] [inst_3 : DecidableEq W] [Nonempty W] (H : SimpleGraph V) (G : SimpleGraph W) [inst_5 : DecidableRel H.Adj] [inst_6 : DecidableRel G.Adj], H.IsBipartite → (completeGraph (Fin 2)).homDensity G ^ #H.edgeFinset ≤ H.homDensity G All goals completed! 🐙

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$.

@[category research open, AMS 5] 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 := ⊢ True ↔ ∀ {V : Type u_3} [inst : Fintype V] [DecidableEq V] (H : SimpleGraph V) [inst_2 : DecidableRel H.Adj], H.IsBipartite → ∀ (W : Graphon), graphonEdgeDensity W ^ #H.edgeFinset ≤ graphonHomDensity H W All goals completed! 🐙

Case: H is a tree (Sidorenko 1993, graphon version).

If H is a finite tree then Sidorenko's inequality holds for all graphons on $[0, 1]$.

@[category research solved, AMS 5] theorem sidorenko_tree_graphon {V : Type*} [Fintype V] [DecidableEq V] (H : SimpleGraph V) [DecidableRel H.Adj] (hTree : H.IsTree) (W : LimitObjects.Graphon) : (graphonEdgeDensity W) ^ H.edgeFinset.card ≤ graphonHomDensity H W := V:Type u_3inst✝²:Fintype Vinst✝¹:DecidableEq VH:SimpleGraph Vinst✝:DecidableRel H.AdjhTree:H.IsTreeW:Graphon⊢ graphonEdgeDensity W ^ #H.edgeFinset ≤ graphonHomDensity H W All goals completed! 🐙

Case: H = C_{2k} is an even cycle (Sidorenko 1993, graphon version).

Every even cycle $C_{2k}$ satisfies Sidorenko's inequality for all graphons on $[0, 1]$.

@[category research solved, AMS 5] theorem sidorenko_even_cycle_graphon (k : ℕ) (hk : 1 ≤ k) (W : LimitObjects.Graphon) : (graphonEdgeDensity W) ^ (cycleGraph (2 * k)).edgeFinset.card ≤ graphonHomDensity (cycleGraph (2 * k)) W := k:ℕhk:1 ≤ kW:Graphon⊢ graphonEdgeDensity W ^ #(cycleGraph (2 * k)).edgeFinset ≤ graphonHomDensity (cycleGraph (2 * k)) W All goals completed! 🐙open scoped Classical in

Case: H = K_{a,b} is a complete bipartite graph (Sidorenko 1993, graphon version).

Every complete bipartite graph $K_{a,b}$ satisfies Sidorenko's inequality for all graphons on $[0, 1]$.

@[category research solved, AMS 5] theorem sidorenko_completeBipartiteGraph_graphon {A B : Type*} [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B] (W : LimitObjects.Graphon) : (graphonEdgeDensity W) ^ (completeBipartiteGraph A B).edgeFinset.card ≤ graphonHomDensity (completeBipartiteGraph A B) W := A:Type u_3B:Type u_4inst✝³:Fintype Ainst✝²:Fintype Binst✝¹:DecidableEq Ainst✝:DecidableEq BW:Graphon⊢ graphonEdgeDensity W ^ #(completeBipartiteGraph A B).edgeFinset ≤ graphonHomDensity (completeBipartiteGraph A B) W All goals completed! 🐙/- ## Tournament Anti-Sidorenko (TAS) Trees Conjecture -/ open scoped Classical in

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$.

@[category research open, AMS 5] 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 := ⊢ True ↔ ∀ {V : Type u_3} [inst : Fintype V] [inst_1 : DecidableEq V] (T : SimpleGraph V) [inst_2 : DecidableRel T.Adj], T.IsTree → ∃ D, D.IsOrientation T ∧ ∀ {W : Type u_4} [inst_3 : Fintype W] [DecidableEq W] [Nonempty W] (G : Digraph W) [inst_6 : DecidableRel G.Adj], G.IsTournament → D.homDensity G ≤ (1 / 2) ^ #T.edgeFinset All goals completed! 🐙open scoped Classical in

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$.

@[category research open, AMS 5] 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 := ⊢ True ↔ ∀ {V : Type u_3} [inst : Fintype V] [DecidableEq V] (T : SimpleGraph V) [inst_2 : DecidableRel T.Adj], T.IsTree → ∃ D, D.IsOrientation T ∧ ∀ (W : Tournamenton), tournamentonHomDensity D W ≤ (1 / 2) ^ #T.edgeFinset All goals completed! 🐙open scoped Classical in

TAS Trees Conjecture: Trees with a single even-degree vertex.

Proven case of TAS Trees Conjecture: any tree containing exactly one vertex of even degree possesses an orientation satisfying the Tournament Anti-Sidorenko inequality $t_{\vec{T}}(G) \le 2^{-e(T)}$.

@[category research solved, AMS 5] theorem tournament_anti_sidorenko_single_even_degree_tree {V : Type*} [Fintype V] [DecidableEq V] (T : SimpleGraph V) [DecidableRel T.Adj] (hTree : T.IsTree) (hEven : (Finset.univ.filter (fun v => Even (T.degree v))).card = 1) : ∃ (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 := V:Type u_3inst✝²:Fintype Vinst✝¹:DecidableEq VT:SimpleGraph Vinst✝:DecidableRel T.AdjhTree:T.IsTreehEven:#{v | Even (T.degree v)} = 1⊢ ∃ D, D.IsOrientation T ∧ ∀ {W : Type u_4} [inst : Fintype W] [DecidableEq W] [Nonempty W] (G : Digraph W) [inst_3 : DecidableRel G.Adj], G.IsTournament → D.homDensity G ≤ (1 / 2) ^ #T.edgeFinset All goals completed! 🐙open scoped Classical in

The $(2,3,4)$-spider tree. A tree composed of three paths of lengths 2, 3, and 4 joined at a single central vertex.

def IsSpider234 {V : Type*} [Fintype V] [DecidableEq V] (T : SimpleGraph V) [DecidableRel T.Adj] : Prop := T.IsTree ∧ Fintype.card V = 10 ∧ ∃ (center l₁ l₂ l₃ : V), T.degree center = 3 ∧ l₁ ≠ l₂ ∧ l₁ ≠ l₃ ∧ l₂ ≠ l₃ ∧ T.degree l₁ = 1 ∧ T.degree l₂ = 1 ∧ T.degree l₃ = 1 ∧ ({T.dist center l₁, T.dist center l₂, T.dist center l₃} : Multiset ℕ) = {2, 3, 4}open scoped Classical in

TAS Trees Conjecture: The $(2,3,4)$-spider tree (Solved case).

The $(2,3,4)$-spider tree satisfies the Tournament Anti-Sidorenko Trees Conjecture.

Reference:

@[category research solved, AMS 5] theorem tournament_anti_sidorenko_spider234 {V : Type*} [Fintype V] [DecidableEq V] (T : SimpleGraph V) [DecidableRel T.Adj] (hSpider : IsSpider234 T) : ∃ (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 := V:Type u_3inst✝²:Fintype Vinst✝¹:DecidableEq VT:SimpleGraph Vinst✝:DecidableRel T.AdjhSpider:IsSpider234 T⊢ ∃ D, D.IsOrientation T ∧ ∀ {W : Type u_4} [inst : Fintype W] [DecidableEq W] [Nonempty W] (G : Digraph W) [inst_3 : DecidableRel G.Adj], G.IsTournament → D.homDensity G ≤ (1 / 2) ^ #T.edgeFinset All goals completed! 🐙

Case H = K_2 (single edge): Sidorenko's inequality holds trivially with equality.

When H is K_2 (the single-edge graph on 2 vertices), e(H) = 1, so the RHS of Sidorenko's inequality is just t(K_2, G)^1 = t(K_2, G) = t(H, G), which equals the LHS. Hence the inequality holds as equality.

The proof records that (completeGraph (Fin 2)).edgeFinset.card = 1 and then reduces the claim to t(K_2, G) ≤ t(K_2, G), which is le_refl.

All goals completed! 🐙/- ## Sidorenko for `K_{2,2}`: auxiliary lemmas -/ open scoped Classical in

edgeCount of K_{2,2} (complete bipartite graph on Fin 2 + Fin 2) is 4.

The four edges are {inl 0, inr 0}, {inl 0, inr 1}, {inl 1, inr 0}, {inl 1, inr 1}.

hdeg:∀ (v : Fin 2 ⊕ Fin 2), (completeBipartiteGraph (Fin 2) (Fin 2)).degree v = 2h:2 * #(completeBipartiteGraph (Fin 2) (Fin 2)).edgeFinset = ∑ v, 2⊢ #(completeBipartiteGraph (Fin 2) (Fin 2)).edgeFinset = 4 hdeg:∀ (v : Fin 2 ⊕ Fin 2), (completeBipartiteGraph (Fin 2) (Fin 2)).degree v = 2h:2 * #(completeBipartiteGraph (Fin 2) (Fin 2)).edgeFinset = 8⊢ #(completeBipartiteGraph (Fin 2) (Fin 2)).edgeFinset = 4 All goals completed! 🐙

Homomorphism count of K_2 into G equals 2 · #edgeFinset.

A homomorphism K_2 →g G is the same data as an ordered pair (f 0, f 1) of distinct vertices with G.Adj (f 0) (f 1). These are in bijection with the Darts of G, and #Darts(G) = 2 · #E(G) by dart_card_eq_twice_card_edges.

W:Type u_3inst✝²:Fintype Winst✝¹:DecidableEq WG:SimpleGraph Winst✝:DecidableRel G.Adj⊢ Fintype.card (completeGraph (Fin 2) →g G) = Fintype.card G.Dart -- Now: `Fintype.card (completeGraph (Fin 2) →g G) = Fintype.card G.Dart`. W:Type u_3inst✝²:Fintype Winst✝¹:DecidableEq WG:SimpleGraph Winst✝:DecidableRel G.Adj⊢ completeGraph (Fin 2) →g G ≃ G.Dart refine { toFun := fun f => ⟨(f 0, f 1), f.map_adj (W:Type u_3inst✝²:Fintype Winst✝¹:DecidableEq WG:SimpleGraph Winst✝:DecidableRel G.Adjf:completeGraph (Fin 2) →g G⊢ (completeGraph (Fin 2)).Adj 0 1 All goals completed! 🐙 : (completeGraph (Fin 2)).Adj 0 1)⟩ invFun := fun d => { toFun := fun i => if i = 0 then d.fst else d.snd map_rel' := fun {a b} hab => W:Type u_3inst✝²:Fintype Winst✝¹:DecidableEq WG:SimpleGraph Winst✝:DecidableRel G.Adjd:G.Darta:Fin 2b:Fin 2hab:(completeGraph (Fin 2)).Adj a b⊢ G.Adj (if a = 0 then d.toProd.1 else d.toProd.2) (if b = 0 then d.toProd.1 else d.toProd.2) -- `completeGraph (Fin 2)` adjacency means `a ≠ b`. W:Type u_3inst✝²:Fintype Winst✝¹:DecidableEq WG:SimpleGraph Winst✝:DecidableRel G.Adjd:G.Darta:Fin 2b:Fin 2hab:a ≠ b⊢ G.Adj (if a = 0 then d.toProd.1 else d.toProd.2) (if b = 0 then d.toProd.1 else d.toProd.2) -- `a, b ∈ Fin 2` with `a ≠ b` means `{a, b} = {0, 1}`. W:Type u_3inst✝²:Fintype Winst✝¹:DecidableEq WG:SimpleGraph Winst✝:DecidableRel G.Adjd:G.Dartb:Fin 2hab:(fun i ↦ i) ⟨0, ⋯⟩ ≠ b⊢ G.Adj (if (fun i ↦ i) ⟨0, ⋯⟩ = 0 then d.toProd.1 else d.toProd.2) (if b = 0 then d.toProd.1 else d.toProd.2)W:Type u_3inst✝²:Fintype Winst✝¹:DecidableEq WG:SimpleGraph Winst✝:DecidableRel G.Adjd:G.Dartb:Fin 2hab:(fun i ↦ i) ⟨1, ⋯⟩ ≠ b⊢ G.Adj (if (fun i ↦ i) ⟨1, ⋯⟩ = 0 then d.toProd.1 else d.toProd.2) (if b = 0 then d.toProd.1 else d.toProd.2) W:Type u_3inst✝²:Fintype Winst✝¹:DecidableEq WG:SimpleGraph Winst✝:DecidableRel G.Adjd:G.Dartb:Fin 2hab:(fun i ↦ i) ⟨0, ⋯⟩ ≠ b⊢ G.Adj (if (fun i ↦ i) ⟨0, ⋯⟩ = 0 then d.toProd.1 else d.toProd.2) (if b = 0 then d.toProd.1 else d.toProd.2)W:Type u_3inst✝²:Fintype Winst✝¹:DecidableEq WG:SimpleGraph Winst✝:DecidableRel G.Adjd:G.Dartb:Fin 2hab:(fun i ↦ i) ⟨1, ⋯⟩ ≠ b⊢ G.Adj (if (fun i ↦ i) ⟨1, ⋯⟩ = 0 then d.toProd.1 else d.toProd.2) (if b = 0 then d.toProd.1 else d.toProd.2) W:Type u_3inst✝²:Fintype Winst✝¹:DecidableEq WG:SimpleGraph Winst✝:DecidableRel G.Adjd:G.Darthab:(fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩⊢ G.Adj (if (fun i ↦ i) ⟨1, ⋯⟩ = 0 then d.toProd.1 else d.toProd.2) (if (fun i ↦ i) ⟨0, ⋯⟩ = 0 then d.toProd.1 else d.toProd.2)W:Type u_3inst✝²:Fintype Winst✝¹:DecidableEq WG:SimpleGraph Winst✝:DecidableRel G.Adjd:G.Darthab:(fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩⊢ G.Adj (if (fun i ↦ i) ⟨1, ⋯⟩ = 0 then d.toProd.1 else d.toProd.2) (if (fun i ↦ i) ⟨1, ⋯⟩ = 0 then d.toProd.1 else d.toProd.2) W:Type u_3inst✝²:Fintype Winst✝¹:DecidableEq WG:SimpleGraph Winst✝:DecidableRel G.Adjd:G.Darthab:(fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩⊢ G.Adj (if (fun i ↦ i) ⟨0, ⋯⟩ = 0 then d.toProd.1 else d.toProd.2) (if (fun i ↦ i) ⟨0, ⋯⟩ = 0 then d.toProd.1 else d.toProd.2) All goals completed! 🐙 W:Type u_3inst✝²:Fintype Winst✝¹:DecidableEq WG:SimpleGraph Winst✝:DecidableRel G.Adjd:G.Darthab:(fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩⊢ G.Adj (if (fun i ↦ i) ⟨0, ⋯⟩ = 0 then d.toProd.1 else d.toProd.2) (if (fun i ↦ i) ⟨1, ⋯⟩ = 0 then d.toProd.1 else d.toProd.2) All goals completed! 🐙 W:Type u_3inst✝²:Fintype Winst✝¹:DecidableEq WG:SimpleGraph Winst✝:DecidableRel G.Adjd:G.Darthab:(fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩⊢ G.Adj (if (fun i ↦ i) ⟨1, ⋯⟩ = 0 then d.toProd.1 else d.toProd.2) (if (fun i ↦ i) ⟨0, ⋯⟩ = 0 then d.toProd.1 else d.toProd.2) All goals completed! 🐙 W:Type u_3inst✝²:Fintype Winst✝¹:DecidableEq WG:SimpleGraph Winst✝:DecidableRel G.Adjd:G.Darthab:(fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩⊢ G.Adj (if (fun i ↦ i) ⟨1, ⋯⟩ = 0 then d.toProd.1 else d.toProd.2) (if (fun i ↦ i) ⟨1, ⋯⟩ = 0 then d.toProd.1 else d.toProd.2) All goals completed! 🐙 } left_inv := fun f => W:Type u_3inst✝²:Fintype Winst✝¹:DecidableEq WG:SimpleGraph Winst✝:DecidableRel G.Adjf:completeGraph (Fin 2) →g G⊢ (fun d ↦ { toFun := fun i ↦ if i = 0 then d.toProd.1 else d.toProd.2, map_rel' := ⋯ }) ((fun f ↦ { fst := f 0, snd := f 1, adj := ⋯ }) f) = f W:Type u_3inst✝²:Fintype Winst✝¹:DecidableEq WG:SimpleGraph Winst✝:DecidableRel G.Adjf:completeGraph (Fin 2) →g Gi:Fin 2⊢ ((fun d ↦ { toFun := fun i ↦ if i = 0 then d.toProd.1 else d.toProd.2, map_rel' := ⋯ }) ((fun f ↦ { fst := f 0, snd := f 1, adj := ⋯ }) f)) i = f i W:Type u_3inst✝²:Fintype Winst✝¹:DecidableEq WG:SimpleGraph Winst✝:DecidableRel G.Adjf:completeGraph (Fin 2) →g G⊢ ((fun d ↦ { toFun := fun i ↦ if i = 0 then d.toProd.1 else d.toProd.2, map_rel' := ⋯ }) ((fun f ↦ { fst := f 0, snd := f 1, adj := ⋯ }) f)) ((fun i ↦ i) ⟨0, ⋯⟩) = f ((fun i ↦ i) ⟨0, ⋯⟩)W:Type u_3inst✝²:Fintype Winst✝¹:DecidableEq WG:SimpleGraph Winst✝:DecidableRel G.Adjf:completeGraph (Fin 2) →g G⊢ ((fun d ↦ { toFun := fun i ↦ if i = 0 then d.toProd.1 else d.toProd.2, map_rel' := ⋯ }) ((fun f ↦ { fst := f 0, snd := f 1, adj := ⋯ }) f)) ((fun i ↦ i) ⟨1, ⋯⟩) = f ((fun i ↦ i) ⟨1, ⋯⟩) W:Type u_3inst✝²:Fintype Winst✝¹:DecidableEq WG:SimpleGraph Winst✝:DecidableRel G.Adjf:completeGraph (Fin 2) →g G⊢ ((fun d ↦ { toFun := fun i ↦ if i = 0 then d.toProd.1 else d.toProd.2, map_rel' := ⋯ }) ((fun f ↦ { fst := f 0, snd := f 1, adj := ⋯ }) f)) ((fun i ↦ i) ⟨0, ⋯⟩) = f ((fun i ↦ i) ⟨0, ⋯⟩)W:Type u_3inst✝²:Fintype Winst✝¹:DecidableEq WG:SimpleGraph Winst✝:DecidableRel G.Adjf:completeGraph (Fin 2) →g G⊢ ((fun d ↦ { toFun := fun i ↦ if i = 0 then d.toProd.1 else d.toProd.2, map_rel' := ⋯ }) ((fun f ↦ { fst := f 0, snd := f 1, adj := ⋯ }) f)) ((fun i ↦ i) ⟨1, ⋯⟩) = f ((fun i ↦ i) ⟨1, ⋯⟩) All goals completed! 🐙 right_inv := fun d => W:Type u_3inst✝²:Fintype Winst✝¹:DecidableEq WG:SimpleGraph Winst✝:DecidableRel G.Adjd:G.Dart⊢ (fun f ↦ { fst := f 0, snd := f 1, adj := ⋯ }) ((fun d ↦ { toFun := fun i ↦ if i = 0 then d.toProd.1 else d.toProd.2, map_rel' := ⋯ }) d) = d W:Type u_3inst✝²:Fintype Winst✝¹:DecidableEq WG:SimpleGraph Winst✝:DecidableRel G.AdjtoProd✝:W × Wadj✝:G.Adj toProd✝.1 toProd✝.2⊢ (fun f ↦ { fst := f 0, snd := f 1, adj := ⋯ }) ((fun d ↦ { toFun := fun i ↦ if i = 0 then d.toProd.1 else d.toProd.2, map_rel' := ⋯ }) { toProd := toProd✝, adj := adj✝ }) = { toProd := toProd✝, adj := adj✝ } All goals completed! 🐙 }open scoped Classical in

The Hom(K_{2,2}, G) decomposition. The number of homomorphisms from K_{2,2} to G equals ∑_{(a, b) ∈ W × W} |N(a) ∩ N(b)|^2, where N(v) is the neighbourhood of v in G. Equivalently, summing over ordered pairs (b₀, b₁) ∈ W × W and counting common neighbours squared.

Math. A homomorphism K_{2,2} →g G is an assignment f : Fin 2 ⊕ Fin 2 → W with G.Adj (f (inl i)) (f (inr j)) for all i, j ∈ Fin 2. Equivalently, choose (a₀, a₁) := (f (inl 0), f (inl 1)) arbitrarily in W × W and require (f (inr 0), f (inr 1)) to both lie in N(a₀) ∩ N(a₁). The count is thus ∑_{(a₀, a₁)} |N(a₀) ∩ N(a₁)|².

Proof. Construct an explicit bijection (K_{2,2} →g G) ≃ Σ (p : W × W), (N(p.1) ∩ N(p.2)) × (N(p.1) ∩ N(p.2)) by sending a homomorphism f to ⟨(f (inl 0), f (inl 1)), ⟨f (inr 0), f (inr 1)⟩⟩. The total cardinality of the sigma-product is then ∑_p (Fintype.card (N(p.1) ∩ N(p.2)))² = ∑_p |N(p.1) ∩ N(p.2)|².

W:Type u_3inst✝²:Fintype Winst✝¹:DecidableEq WG:SimpleGraph Winst✝:DecidableRel G.AdjhNat:(completeBipartiteGraph (Fin 2) (Fin 2)).homCount G = ∑ p, #(G.neighborFinset p.1 ∩ G.neighborFinset p.2) ^ 2⊢ ↑((completeBipartiteGraph (Fin 2) (Fin 2)).homCount G) = ∑ p, ↑(#(G.neighborFinset p.1 ∩ G.neighborFinset p.2)) ^ 2 -- Cast ℕ identity to ℝ. W:Type u_3inst✝²:Fintype Winst✝¹:DecidableEq WG:SimpleGraph Winst✝:DecidableRel G.AdjhNat:(completeBipartiteGraph (Fin 2) (Fin 2)).homCount G = ∑ p, #(G.neighborFinset p.1 ∩ G.neighborFinset p.2) ^ 2this:↑((completeBipartiteGraph (Fin 2) (Fin 2)).homCount G) = ↑(∑ p, #(G.neighborFinset p.1 ∩ G.neighborFinset p.2) ^ 2)⊢ ↑((completeBipartiteGraph (Fin 2) (Fin 2)).homCount G) = ∑ p, ↑(#(G.neighborFinset p.1 ∩ G.neighborFinset p.2)) ^ 2 W:Type u_3inst✝²:Fintype Winst✝¹:DecidableEq WG:SimpleGraph Winst✝:DecidableRel G.AdjhNat:(completeBipartiteGraph (Fin 2) (Fin 2)).homCount G = ∑ p, #(G.neighborFinset p.1 ∩ G.neighborFinset p.2) ^ 2this:↑((completeBipartiteGraph (Fin 2) (Fin 2)).homCount G) = ∑ x, ↑(#(G.neighborFinset x.1 ∩ G.neighborFinset x.2)) ^ 2⊢ ↑((completeBipartiteGraph (Fin 2) (Fin 2)).homCount G) = ∑ p, ↑(#(G.neighborFinset p.1 ∩ G.neighborFinset p.2)) ^ 2 All goals completed! 🐙

K_{2,2} count via a re-indexed sum. Swapping the order of summation, the Hom(K_{2,2}, G) count equals ∑_{a ∈ W} (G.degree a)² summed over... wait, more precisely: the sum ∑_{(b₀, b₁)} |N(b₀) ∩ N(b₁)| (without the square) equals ∑_a (G.degree a)², by swapping (∑_{b₀, b₁} ∑_a [a ~ b₀][a ~ b₁]) = ∑_a (∑_b [a ~ b])².

This version of the identity is what appears in the Cauchy-Schwarz step.

W:Type u_3inst✝²:Fintype Winst✝¹:DecidableEq WG:SimpleGraph Winst✝:DecidableRel G.AdjhNat:∑ p, #(G.neighborFinset p.1 ∩ G.neighborFinset p.2) = ∑ a, G.degree a ^ 2⊢ ∑ p, ↑(#(G.neighborFinset p.1 ∩ G.neighborFinset p.2)) = ∑ a, ↑(G.degree a) ^ 2 -- Cast to ℝ. W:Type u_3inst✝²:Fintype Winst✝¹:DecidableEq WG:SimpleGraph Winst✝:DecidableRel G.AdjhNat:∑ p, #(G.neighborFinset p.1 ∩ G.neighborFinset p.2) = ∑ a, G.degree a ^ 2this:↑(∑ p, #(G.neighborFinset p.1 ∩ G.neighborFinset p.2)) = ↑(∑ a, G.degree a ^ 2)⊢ ∑ p, ↑(#(G.neighborFinset p.1 ∩ G.neighborFinset p.2)) = ∑ a, ↑(G.degree a) ^ 2 W:Type u_3inst✝²:Fintype Winst✝¹:DecidableEq WG:SimpleGraph Winst✝:DecidableRel G.AdjhNat:∑ p, #(G.neighborFinset p.1 ∩ G.neighborFinset p.2) = ∑ a, G.degree a ^ 2this:∑ x, ↑(#(G.neighborFinset x.1 ∩ G.neighborFinset x.2)) = ∑ x, ↑(G.degree x) ^ 2⊢ ∑ p, ↑(#(G.neighborFinset p.1 ∩ G.neighborFinset p.2)) = ∑ a, ↑(G.degree a) ^ 2 All goals completed! 🐙open scoped Classical in

Case H = K_{2,2} (four-cycle, also called C_4): Sidorenko's conjecture holds, by Cauchy–Schwarz.

The textbook statement at H = K_{2,2} is t(K_2, G)^{e(K_{2,2})} = t(K_2, G)^4 ≤ t(K_{2,2}, G).

Proof sketch. Write d(a) := G.degree a. Then

    homCount(K_2, G) = ∑_a d(a) = 2·|E(G)| (handshaking).

    homCount(K_{2,2}, G) = ∑_{b₀, b₁} |N(b₀) ∩ N(b₁)|² (product structure of bipartite homomorphism).

    ∑_{b₀, b₁} |N(b₀) ∩ N(b₁)| = ∑_a d(a)² (swap sums).

    Cauchy–Schwarz #1: (∑_{b₀, b₁} |N(b₀) ∩ N(b₁)|)² ≤ |W|² · ∑_{b₀, b₁} |N(b₀) ∩ N(b₁)|².

    Cauchy–Schwarz #2: (∑_a d(a))² ≤ |W| · ∑_a d(a)².

    Chain: (∑_a d(a))⁴ ≤ |W|⁴ · homCount(K_{2,2}, G).

    Divide by |W|^8 to get t(K_2, G)^4 ≤ t(K_{2,2}, G).

The proof uses Finset.sum_mul_sq_le_sq_mul_sq (discrete Cauchy–Schwarz) from Mathlib.Algebra.Order.BigOperators.Ring.Finset.

Status (2026-04-22): main theorem closed sorry-free. See [Si93].

W:Typeinst✝²:Fintype Winst✝¹:DecidableEq WG:SimpleGraph Winst✝:DecidableRel G.AdjhW:¬IsEmpty Wthis:Nonempty Wn:ℕ := Fintype.card WhWpos:0 < ↑nhn:n = Fintype.card Whn_pos:0 < ↑nhFin2:Fintype.card (Fin 2) = 2hFin2sum:Fintype.card (Fin 2 ⊕ Fin 2) = 4N:ℕ := (completeGraph (Fin 2)).homCount GhN:N = (completeGraph (Fin 2)).homCount GM:ℕ := (completeBipartiteGraph (Fin 2) (Fin 2)).homCount GhM:M = (completeBipartiteGraph (Fin 2) (Fin 2)).homCount Gh_main:↑N ^ 4 ≤ ↑M * ↑n ^ 4hn4_pos:0 < ↑n ^ 4hn2_pos:0 < ↑n ^ 2⊢ ↑N ^ 4 * ↑n ^ 4 ≤ ↑M * (↑n ^ 2) ^ 4 -- Goal: N^4 * n^4 ≤ M * (n^2)^4 = M * n^8. -- From h_main: N^4 ≤ M * n^4. Multiply both sides by n^4 > 0. W:Typeinst✝²:Fintype Winst✝¹:DecidableEq WG:SimpleGraph Winst✝:DecidableRel G.AdjhW:¬IsEmpty Wthis:Nonempty Wn:ℕ := Fintype.card WhWpos:0 < ↑nhn:n = Fintype.card Whn_pos:0 < ↑nhFin2:Fintype.card (Fin 2) = 2hFin2sum:Fintype.card (Fin 2 ⊕ Fin 2) = 4N:ℕ := (completeGraph (Fin 2)).homCount GhN:N = (completeGraph (Fin 2)).homCount GM:ℕ := (completeBipartiteGraph (Fin 2) (Fin 2)).homCount GhM:M = (completeBipartiteGraph (Fin 2) (Fin 2)).homCount Gh_main:↑N ^ 4 ≤ ↑M * ↑n ^ 4hn4_pos:0 < ↑n ^ 4hn2_pos:0 < ↑n ^ 2hmul:↑N ^ 4 * ↑n ^ 4 ≤ ↑M * ↑n ^ 4 * ↑n ^ 4⊢ ↑N ^ 4 * ↑n ^ 4 ≤ ↑M * (↑n ^ 2) ^ 4 -- hmul : N^4 * n^4 ≤ (M * n^4) * n^4 All goals completed! 🐙open scoped Classical in

Consequence of homDensity_le_one: both sides of the Sidorenko K_{2,2} inequality are bounded above by 1. This is a trivial consequence, recorded as a sanity check on the helper infrastructure in FormalConjecturesForMathlib.Combinatorics.SimpleGraph.HomDensity.

@[category API, AMS 5] theorem sidorenko_K22_both_sides_bounded {W : Type*} [Fintype W] [Nonempty W] [DecidableEq W] (G : SimpleGraph W) [DecidableRel G.Adj] : homDensity (completeGraph (Fin 2)) G ≤ 1 ∧ homDensity (completeBipartiteGraph (Fin 2) (Fin 2)) G ≤ 1 := ⟨SimpleGraph.homDensity_le_one _ _, SimpleGraph.homDensity_le_one _ _⟩

If the domain of H has at most one vertex, H has no edges.

Proof. SimpleGraph.Adj is irreflexive, so any adjacency H.Adj u v forces u ≠ v; on a subsingleton that's impossible, so no edges exist.

V:Type u_3inst✝²:Fintype Vinst✝¹:Subsingleton VH:SimpleGraph Vinst✝:DecidableRel H.Adju:Vv:Vhe:H.Adj u v⊢ False All goals completed! 🐙

If the domain of H has at most one vertex, every function V → W is a homomorphism H →g G. Equivalently, homCount H G = |W|^|V|.

Proof. The adjacency H.Adj u v is irreflexive; on a subsingleton it is uninhabited, so the homomorphism condition H.Adj u v → G.Adj (f u) (f v) is vacuous. Hence the coe : (H →g G) → (V → W) map is a bijection.

V:Type u_3W:Type u_4inst✝⁶:Fintype Vinst✝⁵:Fintype Winst✝⁴:Subsingleton Vinst✝³:DecidableEq Vinst✝²:DecidableEq WH:SimpleGraph VG:SimpleGraph Winst✝¹:DecidableRel H.Adjinst✝:DecidableRel G.Adj⊢ Fintype.card (H →g G) = Fintype.card (V → W) V:Type u_3W:Type u_4inst✝⁶:Fintype Vinst✝⁵:Fintype Winst✝⁴:Subsingleton Vinst✝³:DecidableEq Vinst✝²:DecidableEq WH:SimpleGraph VG:SimpleGraph Winst✝¹:DecidableRel H.Adjinst✝:DecidableRel G.Adj⊢ H →g G ≃ (V → W) All goals completed! 🐙

Base case of Sidorenko for trees. When the tree H has at most one vertex, both sides of Sidorenko's inequality evaluate to 1 (there are no edges, and every function is a homomorphism). Thus the inequality 1 ≤ 1 holds trivially.

This covers the |V(T)| = 1 base case of the induction on tree size.

All goals completed! 🐙

Case: H is a tree (Sidorenko 1993).

If H is a finite tree then Sidorenko's inequality holds.

Proof idea (Sidorenko 1993): by induction on the tree, applying Jensen / convexity. The number of homomorphisms from a tree T with v vertices and v - 1 edges into G factors nicely in the degree sequence of G, and AM–GM / convexity gives the required lower bound.

Current status (2026-04-22, partial):

    The subsingleton base case (|V(T)| ≤ 1) is dispatched via sidorenko_tree_subsingleton.

    The main inductive step (leaf extraction + AM–GM on the degree sequence) is deferred; it requires a walk-parametrised homomorphism count for trees and a discrete Jensen inequality. See [Si93].

The full proof is left as sorry; the subsingleton case is closed.

@[category research solved, AMS 5] theorem sidorenko_tree {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] (hTree : H.IsTree) : homDensity (completeGraph (Fin 2)) G ^ (H.edgeFinset.card) ≤ homDensity H G := V:TypeW:Typeinst✝⁶:Fintype Vinst✝⁵:Fintype Winst✝⁴:DecidableEq Vinst✝³:DecidableEq Winst✝²:Nonempty WH:SimpleGraph VG:SimpleGraph Winst✝¹:DecidableRel H.Adjinst✝:DecidableRel G.AdjhTree:H.IsTree⊢ (completeGraph (Fin 2)).homDensity G ^ #H.edgeFinset ≤ H.homDensity G -- A tree's vertex set is nonempty. V:TypeW:Typeinst✝⁶:Fintype Vinst✝⁵:Fintype Winst✝⁴:DecidableEq Vinst✝³:DecidableEq Winst✝²:Nonempty WH:SimpleGraph VG:SimpleGraph Winst✝¹:DecidableRel H.Adjinst✝:DecidableRel G.AdjhTree:H.IsTreethis:Nonempty V⊢ (completeGraph (Fin 2)).homDensity G ^ #H.edgeFinset ≤ H.homDensity G -- Split on whether `V` is a subsingleton. V:TypeW:Typeinst✝⁶:Fintype Vinst✝⁵:Fintype Winst✝⁴:DecidableEq Vinst✝³:DecidableEq Winst✝²:Nonempty WH:SimpleGraph VG:SimpleGraph Winst✝¹:DecidableRel H.Adjinst✝:DecidableRel G.AdjhTree:H.IsTreethis:Nonempty VhSub:Subsingleton V⊢ (completeGraph (Fin 2)).homDensity G ^ #H.edgeFinset ≤ H.homDensity GV:TypeW:Typeinst✝⁶:Fintype Vinst✝⁵:Fintype Winst✝⁴:DecidableEq Vinst✝³:DecidableEq Winst✝²:Nonempty WH:SimpleGraph VG:SimpleGraph Winst✝¹:DecidableRel H.Adjinst✝:DecidableRel G.AdjhTree:H.IsTreethis:Nonempty VhSub:¬Subsingleton V⊢ (completeGraph (Fin 2)).homDensity G ^ #H.edgeFinset ≤ H.homDensity G V:TypeW:Typeinst✝⁶:Fintype Vinst✝⁵:Fintype Winst✝⁴:DecidableEq Vinst✝³:DecidableEq Winst✝²:Nonempty WH:SimpleGraph VG:SimpleGraph Winst✝¹:DecidableRel H.Adjinst✝:DecidableRel G.AdjhTree:H.IsTreethis:Nonempty VhSub:Subsingleton V⊢ (completeGraph (Fin 2)).homDensity G ^ #H.edgeFinset ≤ H.homDensity G -- Base case: `|V| ≤ 1`, so `H` has no edges and both sides equal `1`. All goals completed! 🐙 V:TypeW:Typeinst✝⁶:Fintype Vinst✝⁵:Fintype Winst✝⁴:DecidableEq Vinst✝³:DecidableEq Winst✝²:Nonempty WH:SimpleGraph VG:SimpleGraph Winst✝¹:DecidableRel H.Adjinst✝:DecidableRel G.AdjhTree:H.IsTreethis:Nonempty VhSub:¬Subsingleton V⊢ (completeGraph (Fin 2)).homDensity G ^ #H.edgeFinset ≤ H.homDensity G -- Inductive step: `|V| ≥ 2`. This is the AM–GM / Jensen part of Sidorenko's proof. -- The argument: pick a leaf `v` of `H`, set `H' := H \ {v}` (a tree on `|V|-1` -- vertices), apply IH, then use the leaf decomposition -- `homCount H G = ∑ {φ : H' →g G}, G.degree (φ u)` (where `u` is the unique neighbour -- of `v` in `H`) and discrete Jensen on the degree sequence. -- -- This requires: -- 1. A `homCount_of_leaf_decomposition` lemma (sum over `φ : H' →g G` of `G.degree (φ u)`). -- 2. A discrete Jensen inequality (`∑ x_i · w_i ≥ (∑ w_i) · ((∑ x_i w_i) / ∑ w_i)` with -- appropriate convexity). -- 3. Induction on `H.edgeFinset.card` (equivalently `|V| - 1`). -- -- Deferred to a future commit; see `docs/PHASE2_PROOF_ROADMAP.md` §6. All goals completed! 🐙

Case: complete bipartite graphs K_{s,t} (Sidorenko 1993).

Sidorenko's inequality holds when H = K_{s,t} is a complete bipartite graph. This is one of the earliest known cases; it follows from repeated applications of the Cauchy–Schwarz / Hölder inequality. The s = t = 2 instance is sidorenko_K22.

Reference: [Si93].

@[category research solved, AMS 5] theorem sidorenko_conjecture.variants.complete_bipartite (s t : ℕ) [DecidableRel (completeBipartiteGraph (Fin s) (Fin t)).Adj] {W : Type} [Fintype W] [DecidableEq W] [Nonempty W] (G : SimpleGraph W) [DecidableRel G.Adj] : homDensity (completeGraph (Fin 2)) G ^ ((completeBipartiteGraph (Fin s) (Fin t)).edgeFinset.card) ≤ homDensity (completeBipartiteGraph (Fin s) (Fin t)) G := s:ℕt:ℕinst✝⁴:DecidableRel (completeBipartiteGraph (Fin s) (Fin t)).AdjW:Typeinst✝³:Fintype Winst✝²:DecidableEq Winst✝¹:Nonempty WG:SimpleGraph Winst✝:DecidableRel G.Adj⊢ (completeGraph (Fin 2)).homDensity G ^ #(completeBipartiteGraph (Fin s) (Fin t)).edgeFinset ≤ (completeBipartiteGraph (Fin s) (Fin t)).homDensity G All goals completed! 🐙

Case: even cycles C_{2k} (Sidorenko 1993).

Sidorenko's inequality holds for every even cycle C_{2k} with k ≥ 2 (cycleGraph (2 * k)). Even cycles are bipartite; the k = 2 case C_4 coincides with K_{2,2} (sidorenko_K22).

Reference: [Si93].

@[category research solved, AMS 5] theorem sidorenko_conjecture.variants.even_cycle (k : ℕ) (hk : 2 ≤ k) {W : Type} [Fintype W] [DecidableEq W] [Nonempty W] (G : SimpleGraph W) [DecidableRel G.Adj] : homDensity (completeGraph (Fin 2)) G ^ ((cycleGraph (2 * k)).edgeFinset.card) ≤ homDensity (cycleGraph (2 * k)) G := k:ℕhk:2 ≤ kW:Typeinst✝³:Fintype Winst✝²:DecidableEq Winst✝¹:Nonempty WG:SimpleGraph Winst✝:DecidableRel G.Adj⊢ (completeGraph (Fin 2)).homDensity G ^ #(cycleGraph (2 * k)).edgeFinset ≤ (cycleGraph (2 * k)).homDensity G All goals completed! 🐙

Case: paths, the Blakley–Roy inequality (1965).

For the path P_n on n vertices (pathGraph n), Sidorenko's inequality t(K_2, G)^{e(P_n)} ≤ t(P_n, G) is the Blakley–Roy inequality, established well before Sidorenko's general conjecture. Paths are trees, so this is also a special case of sidorenko_tree.

Reference: [BR65].

@[category research solved, AMS 5] theorem sidorenko_conjecture.variants.path_blakley_roy (n : ℕ) [DecidableRel (pathGraph n).Adj] {W : Type} [Fintype W] [DecidableEq W] [Nonempty W] (G : SimpleGraph W) [DecidableRel G.Adj] : homDensity (completeGraph (Fin 2)) G ^ ((pathGraph n).edgeFinset.card) ≤ homDensity (pathGraph n) G := n:ℕinst✝⁴:DecidableRel (pathGraph n).AdjW:Typeinst✝³:Fintype Winst✝²:DecidableEq Winst✝¹:Nonempty WG:SimpleGraph Winst✝:DecidableRel G.Adj⊢ (completeGraph (Fin 2)).homDensity G ^ #(pathGraph n).edgeFinset ≤ (pathGraph n).homDensity G All goals completed! 🐙

Homomorphism count of the star K_{1,m}. The number of homomorphisms from the star K_{1,m} = completeBipartiteGraph (Fin 1) (Fin m) into G equals ∑_{c} (G.degree c)^m.

Math. A homomorphism f : K_{1,m} →g G is determined by the image c := f of the centre Sum.inl 0 together with the images of the m leaves Sum.inr j, each of which must lie in the neighbourhood N(c) (and there is no constraint between distinct leaves). So the data is a choice of c and a function Fin m → N(c), giving ∑_c |N(c)|^m = ∑_c (G.degree c)^m.

All goals completed! 🐙

Edge count of the star K_{1,m}. The star completeBipartiteGraph (Fin 1) (Fin m) has exactly m edges (the centre Sum.inl 0 joined to each of the m leaves).

m:ℕinst✝:DecidableRel (completeBipartiteGraph (Fin 1) (Fin m)).Adjhdeg_centre:(completeBipartiteGraph (Fin 1) (Fin m)).degree (Sum.inl 0) = mhdeg_leaf:∀ (j : Fin m), (completeBipartiteGraph (Fin 1) (Fin m)).degree (Sum.inr j) = 1hsum:∑ v, (completeBipartiteGraph (Fin 1) (Fin m)).degree v = 2 * mh:2 * m = 2 * #(completeBipartiteGraph (Fin 1) (Fin m)).edgeFinset⊢ #(completeBipartiteGraph (Fin 1) (Fin m)).edgeFinset = m All goals completed! 🐙

Case: stars K_{1,m} (Sidorenko).

Sidorenko's inequality holds for every star K_{1,m} = completeBipartiteGraph (Fin 1) (Fin m). This is a fully proved instance of both sidorenko_conjecture.variants.complete_bipartite and sidorenko_tree (a star is a complete bipartite graph and a tree).

Proof. With d(c) := G.degree c and N := |W|, the star has m edges, so the desired inequality is (∑_c d(c) / N^2)^m ≤ (∑_c d(c)^m) / N^{m+1} (using t(K_2, G) = ∑_c d(c) / N^2 and t(K_{1,m}, G) = ∑_c d(c)^m / N^{m+1} via homCount_star_eq_sum_degree_pow). After clearing denominators this is (∑_c d(c))^m ≤ N^{m-1} · ∑_c d(c)^m, the power-mean (Jensen) inequality Finset.pow_sum_div_card_le_sum_pow.

W:Typeinst✝⁴:Fintype Winst✝³:DecidableEq Winst✝²:Nonempty WG:SimpleGraph Winst✝¹:DecidableRel G.AdjN:ℕ := Fintype.card WhN:N = Fintype.card WhNpos:0 < ↑NhLbase:(completeGraph (Fin 2)).homDensity G = (∑ c, ↑(G.degree c)) / ↑N ^ 2k:ℕinst✝:DecidableRel (completeBipartiteGraph (Fin 1) (Fin k.succ)).AdjhR:(completeBipartiteGraph (Fin 1) (Fin k.succ)).homDensity G = (∑ c, ↑(G.degree c) ^ k.succ) / ↑N ^ (k.succ + 1)hm:k.succ > 0hjensen:(∑ i, ↑(G.degree i)) ^ (k + 1) ≤ (∑ i, ↑(G.degree i) ^ (k + 1)) * ↑N ^ k⊢ (∑ c, ↑(G.degree c)) ^ k.succ * ↑N ^ (k.succ + 1) ≤ (∑ c, ↑(G.degree c) ^ k.succ) * (↑N ^ 2) ^ k.succ calc (∑ c : W, (G.degree c : ℝ)) ^ (k + 1) * (N : ℝ) ^ (k + 1 + 1) ≤ ((∑ c : W, (G.degree c : ℝ) ^ (k + 1)) * (N : ℝ) ^ k) * (N : ℝ) ^ (k + 1 + 1) := mul_le_mul_of_nonneg_right hjensen (W:Typeinst✝⁴:Fintype Winst✝³:DecidableEq Winst✝²:Nonempty WG:SimpleGraph Winst✝¹:DecidableRel G.AdjN:ℕ := Fintype.card WhN:N = Fintype.card WhNpos:0 < ↑NhLbase:(completeGraph (Fin 2)).homDensity G = (∑ c, ↑(G.degree c)) / ↑N ^ 2k:ℕinst✝:DecidableRel (completeBipartiteGraph (Fin 1) (Fin k.succ)).AdjhR:(completeBipartiteGraph (Fin 1) (Fin k.succ)).homDensity G = (∑ c, ↑(G.degree c) ^ k.succ) / ↑N ^ (k.succ + 1)hm:k.succ > 0hjensen:(∑ i, ↑(G.degree i)) ^ (k + 1) ≤ (∑ i, ↑(G.degree i) ^ (k + 1)) * ↑N ^ k⊢ 0 ≤ ↑N ^ (k + 1 + 1) All goals completed! 🐙) _ = (∑ c : W, (G.degree c : ℝ) ^ (k + 1)) * ((N : ℝ) ^ 2) ^ (k + 1) := W:Typeinst✝⁴:Fintype Winst✝³:DecidableEq Winst✝²:Nonempty WG:SimpleGraph Winst✝¹:DecidableRel G.AdjN:ℕ := Fintype.card WhN:N = Fintype.card WhNpos:0 < ↑NhLbase:(completeGraph (Fin 2)).homDensity G = (∑ c, ↑(G.degree c)) / ↑N ^ 2k:ℕinst✝:DecidableRel (completeBipartiteGraph (Fin 1) (Fin k.succ)).AdjhR:(completeBipartiteGraph (Fin 1) (Fin k.succ)).homDensity G = (∑ c, ↑(G.degree c) ^ k.succ) / ↑N ^ (k.succ + 1)hm:k.succ > 0hjensen:(∑ i, ↑(G.degree i)) ^ (k + 1) ≤ (∑ i, ↑(G.degree i) ^ (k + 1)) * ↑N ^ k⊢ (∑ c, ↑(G.degree c) ^ (k + 1)) * ↑N ^ k * ↑N ^ (k + 1 + 1) = (∑ c, ↑(G.degree c) ^ (k + 1)) * (↑N ^ 2) ^ (k + 1) All goals completed! 🐙

Bipartiteness is necessary: the triangle is not a Sidorenko graph.

The hypothesis H.IsBipartite in sidorenko_conjecture cannot be dropped. For the triangle H = K_3 (chromatic number 3, hence not bipartite) and the single edge G = K_2, Sidorenko's inequality fails: the putative lower bound is t(K_2, K_2)^{e(K_3)} = (1/2)^3 = 1/8, while the actual density is t(K_3, K_2) = 0, because there is no graph homomorphism from K_3 into the triangle-free graph K_2 (such a homomorphism would be an injection Fin 3 ↪ Fin 2). So the lower bound 1/8 strictly exceeds the true value 0.

More generally, any H containing an odd cycle fails Sidorenko's inequality against a suitable bipartite G, since then t(H, G) = 0 < t(K_2, G)^{e(H)}.

hK3edges:#(completeGraph (Fin 3)).edgeFinset = 3hRHSbase:(completeGraph (Fin 2)).homDensity (completeGraph (Fin 2)) = 1 / 2hLHS:(completeGraph (Fin 3)).homDensity (completeGraph (Fin 2)) = 0⊢ 0 < (1 / 2) ^ 3 All goals completed! 🐙end SidorenkoConjecture