SidorenkoConjecture.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

28 declarations, 13 contain sorry, 0 declared as axioms

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.

Imports (1)

FormalConjecturesUtil

theorem SidorenkoConjecture.sidorenko_conjecture Sidorenko's conjecture (1993) sorry line 63 source
Source documentation
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)).

depends on sorry what this means
Statement uses: Iff, True, Fintype, DecidableEq, Nonempty, SimpleGraph, DecidableRel, SimpleGraph.Adj, SimpleGraph.IsBipartite, LE.le, Real, HPow.hPow, Nat, SimpleGraph.homDensity, Fin, OfNat.ofNat, SimpleGraph.completeGraph, Finset.card, Sym2, SimpleGraph.edgeFinset
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
22 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
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 := by
…
```
theorem SidorenkoConjecture.sidorenko_conjecture_graphon Sidorenko's conjecture for graphons (1993) sorry line 79 source
Source documentation
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$.

depends on sorry what this means
Statement uses: Iff, True, Fintype, DecidableEq, SimpleGraph, DecidableRel, SimpleGraph.Adj, SimpleGraph.IsBipartite, LimitObjects.Graphon, LE.le, Real, HPow.hPow, Nat, LimitObjects.graphonEdgeDensity, Finset.card, Sym2, SimpleGraph.edgeFinset, LimitObjects.graphonHomDensity
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat
15 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
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 := by
…
```
theorem SidorenkoConjecture.sidorenko_tree_graphon Case: H is a tree (Sidorenko 1993, graphon version) sorry line 94 source
Source documentation
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]$.

depends on sorry what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, DecidableRel, SimpleGraph.Adj, SimpleGraph.IsTree, LimitObjects.Graphon, LE.le, Real, HPow.hPow, Nat, LimitObjects.graphonEdgeDensity, Finset.card, Sym2, SimpleGraph.edgeFinset, LimitObjects.graphonHomDensity
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat
15 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
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 := by
…
```
Mentions: LimitObjects.Graphon
theorem SidorenkoConjecture.sidorenko_even_cycle_graphon Case: H = C_{2k} is an even cycle (Sidorenko 1993, graphon version) sorry line 106 source
Source documentation
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]$.

depends on sorry what this means
Statement uses: Nat, LE.le, OfNat.ofNat, LimitObjects.Graphon, Real, HPow.hPow, LimitObjects.graphonEdgeDensity, Finset.card, Sym2, Fin, HMul.hMul, SimpleGraph.edgeFinset, SimpleGraph.cycleGraph, LimitObjects.graphonHomDensity
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
26 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem sidorenko_even_cycle_graphon (k : ℕ) (hk : 1 ≤ k)
    (W : LimitObjects.Graphon) :
    (graphonEdgeDensity W) ^ (cycleGraph (2 * k)).edgeFinset.card ≤
      graphonHomDensity (cycleGraph (2 * k)) W := by
…
```
Mentions: LimitObjects.Graphon
theorem SidorenkoConjecture.sidorenko_completeBipartiteGraph_graphon Case: H = K_{a,b} is a complete bipartite graph (Sidorenko 1993, graphon version) sorry line 119 source
Source documentation
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]$.

depends on sorry what this means
Statement uses: Fintype, DecidableEq, LimitObjects.Graphon, LE.le, Real, HPow.hPow, Nat, LimitObjects.graphonEdgeDensity, Finset.card, Sym2, Sum, SimpleGraph.edgeFinset, completeBipartiteGraph, Classical.propDecidable, SimpleGraph.Adj, LimitObjects.graphonHomDensity
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat
17 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
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 := by
…
```
Mentions: LimitObjects.Graphon
theorem SidorenkoConjecture.tournament_anti_sidorenko_trees_conjecture Tournament Anti-Sidorenko (TAS) Trees Conjecture sorry line 137 source
Source documentation
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$.

depends on sorry what this means
Statement uses: Iff, True, Fintype, DecidableEq, SimpleGraph, DecidableRel, SimpleGraph.Adj, SimpleGraph.IsTree, Exists, Digraph, And, Digraph.IsOrientation, Nonempty, Digraph.Adj, Digraph.IsTournament, LE.le, Real, Digraph.homDensity, Classical.propDecidable, HPow.hPow and 6 more
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
34 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
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 := by
…
```
Mentions: Digraph.homDensity
theorem SidorenkoConjecture.tournament_anti_sidorenko_trees_conjecture_tournamenton Tournament Anti-Sidorenko (TAS) Trees Conjecture (Tournamenton limit version) sorry line 158 source
Source documentation
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$.

depends on sorry what this means
Statement uses: Iff, True, Fintype, DecidableEq, SimpleGraph, DecidableRel, SimpleGraph.Adj, SimpleGraph.IsTree, Exists, Digraph, And, Digraph.IsOrientation, LimitObjects.Tournamenton, LE.le, Real, LimitObjects.tournamentonHomDensity, Classical.propDecidable, Digraph.Adj, HPow.hPow, Nat and 5 more
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
34 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
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 := by
…
```
Mentions: LimitObjects.Tournamenton
theorem SidorenkoConjecture.tournament_anti_sidorenko_single_even_degree_tree TAS Trees Conjecture: Trees with a single even-degree vertex sorry line 175 source
Source documentation
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)}$.

depends on sorry what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, DecidableRel, SimpleGraph.Adj, SimpleGraph.IsTree, Eq, Nat, Finset.card, Finset.filter, Even, SimpleGraph.degree, Membership.mem, Set, SimpleGraph.neighborSet, Finset.univ, OfNat.ofNat, Exists, Digraph, And and 12 more
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
44 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
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 := by
…
```
Mentions: Digraph.homDensity
def SidorenkoConjecture.IsSpider234 The $(2,3,4)$-spider tree line 193 source
Source documentation
The $(2,3,4)$-spider tree. A tree composed of three paths of lengths 2, 3, and 4 joined at a single central vertex: the centre is the unique vertex of degree 3 (every other vertex has degree at most 2), so the tree has exactly three leaves, at distances 2, 3 and 4 from the centre.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, DecidableRel, SimpleGraph.Adj
Proof uses: And, SimpleGraph.IsTree, Eq, Nat, Fintype.card, OfNat.ofNat, Exists, SimpleGraph.degree, Membership.mem, Set, SimpleGraph.neighborSet, Ne, LE.le, Multiset, Insert.insert, SimpleGraph.dist, Singleton.singleton
7 instances, coercions and auxiliary constants left out.
```
def IsSpider234 {V : Type*} [Fintype V] [DecidableEq V] (T : SimpleGraph V) [DecidableRel T.Adj] : Prop :=
…
```
theorem SidorenkoConjecture.tournament_anti_sidorenko_spider234 TAS Trees Conjecture: The $(2,3,4)$-spider tree (Solved case) sorry line 212 source
Source documentation
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:
- ArXiv 2605.14138
L4DEL explanation
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: * ArXiv 2605.14138
Sources and attribution: Pinned Lean source (1646ca16afd6)

depends on sorry what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, DecidableRel, SimpleGraph.Adj, SidorenkoConjecture.IsSpider234, Exists, Digraph, And, Digraph.IsOrientation, Nonempty, Digraph.Adj, Digraph.IsTournament, LE.le, Real, Digraph.homDensity, Classical.propDecidable, HPow.hPow, Nat, HDiv.hDiv and 4 more
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
34 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
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 := by
…
```
Mentions: SidorenkoConjecture.IsSpider234, Digraph.homDensity
theorem SidorenkoConjecture.sidorenko_K2 Case H = K_2 (single edge): Sidorenko's inequality holds trivially with equality line 235 source
Source documentation
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.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, DecidableRel, SimpleGraph.Adj, LE.le, Real, HPow.hPow, Nat, SimpleGraph.homDensity, Fin, OfNat.ofNat, SimpleGraph.completeGraph, Finset.card, Sym2, SimpleGraph.edgeFinset
Proof uses: Eq, Eq.mpr, Nat.choose, id, congrArg, SimpleGraph.card_edgeFinset_completeGraph_fin, Nat.choose_self, Eq.refl, pow_one, le_refl
23 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
theorem sidorenko_K2 {W : Type} [Fintype W] [DecidableEq W]
    (G : SimpleGraph W) [DecidableRel G.Adj] :
    homDensity (completeGraph (Fin 2)) G ^
      ((completeGraph (Fin 2)).edgeFinset.card) ≤
      homDensity (completeGraph (Fin 2)) G := by
…
```
lemma SidorenkoConjecture.edgeCount_completeBipartiteGraph_fin_two edgeCount of K_{2,2} (complete bipartite graph on Fin 2 + Fin 2) is 4 line 252 source
Source documentation
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}.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Finset.card, Sym2, Sum, Fin, OfNat.ofNat, SimpleGraph.edgeFinset, completeBipartiteGraph, Classical.propDecidable, SimpleGraph.Adj
Proof uses: SimpleGraph.degree, Membership.mem, Set, SimpleGraph.neighborSet, Eq.mpr, SimpleGraph.neighborFinset, id, congrArg, rfl, Sum.inl, Finset.filter, Finset.univ, Finset, SimpleGraph.neighborFinset_eq_filter, Insert.insert, Sum.inr, Singleton.singleton, Finset.ext, Iff, of_eq_true and 64 more
42 instances, coercions and auxiliary constants left out.

Tactic trace: 31 steps
Open to load the checked before-and-after goal states.
```
lemma edgeCount_completeBipartiteGraph_fin_two :
    (completeBipartiteGraph (Fin 2) (Fin 2)).edgeFinset.card = 4 := by
…
```
lemma SidorenkoConjecture.homCount_completeGraph_fin_two_eq_two_mul_card_edgeFinset Homomorphism count of K_2 into G equals 2 · #edgeFinset line 301 source
Source documentation
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.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, DecidableRel, SimpleGraph.Adj, Eq, Nat, SimpleGraph.homCount, Fin, OfNat.ofNat, SimpleGraph.completeGraph, HMul.hMul, Finset.card, Sym2, SimpleGraph.edgeFinset
Proof uses: id, Eq.mpr, Fintype.card, SimpleGraph.Hom, SimpleGraph.Dart, congrArg, Eq.symm, SimpleGraph.dart_card_eq_twice_card_edges, Fintype.card_congr, Equiv.mk, SimpleGraph.Dart.mk, Prod.mk, SimpleGraph.Hom.map_adj, of_decide_eq_true, Bool, Decidable.decide, Bool.true, Eq.refl, RelHom.mk, ite and 45 more
49 instances, coercions and auxiliary constants left out.

Tactic trace: 21 steps
Open to load the checked before-and-after goal states.
```
lemma homCount_completeGraph_fin_two_eq_two_mul_card_edgeFinset
    {W : Type*} [Fintype W] [DecidableEq W]
    (G : SimpleGraph W) [DecidableRel G.Adj] :
    homCount (completeGraph (Fin 2)) G = 2 * #G.edgeFinset := by
…
```
lemma SidorenkoConjecture.homCount_completeBipartiteGraph_fin_two_eq_sum_inter_sq The Hom(K_{2,2}, G) decomposition line 349 source
Source documentation
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)|².

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, DecidableRel, SimpleGraph.Adj, Eq, Real, SimpleGraph.homCount, Sum, Fin, OfNat.ofNat, Nat, completeBipartiteGraph, Classical.propDecidable, Finset.sum, Prod, Finset.univ, HPow.hPow, Finset.card, Inter.inter and 7 more
Proof uses: id, Equiv, SimpleGraph.Hom, Sigma, Subtype, Equiv.mk, Sigma.mk, Prod.mk, Sum.inl, Subtype.mk, Sum.inr, Eq.mpr, And, Eq.trans, congr, congrArg, And.intro, SimpleGraph.Hom.map_adj, of_eq_true, Or and 51 more
67 instances, coercions and auxiliary constants left out.

Tactic trace: 53 steps
Open to load the checked before-and-after goal states.
```
lemma homCount_completeBipartiteGraph_fin_two_eq_sum_inter_sq
    {W : Type*} [Fintype W] [DecidableEq W]
    (G : SimpleGraph W) [DecidableRel G.Adj] :
    (homCount (completeBipartiteGraph (Fin 2) (Fin 2)) G : ℝ) =
      ∑ p : W × W,
        (((G.neighborFinset p.1) ∩ (G.neighborFinset p.2)).card : ℝ) ^ 2 := by
…
```
lemma SidorenkoConjecture.sum_inter_card_eq_sum_degree_sq K_{2,2} count via a re-indexed sum line 438 source
Source documentation
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.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, DecidableRel, SimpleGraph.Adj, Eq, Real, Finset.sum, Prod, Finset.univ, Finset.card, Inter.inter, Finset, SimpleGraph.neighborFinset, Prod.fst, Membership.mem, Set, SimpleGraph.neighborSet, Prod.snd, HPow.hPow and 3 more
Proof uses: Trans.trans, ite, And, Finset.filter, Finset.sum_congr, rfl, Eq.rec, Eq.refl, Finset.ext, of_eq_true, Iff, Eq.trans, True, congr, congrArg, congrFun', Finset.filter_congr, Iff.of_eq, true_and, iff_self and 37 more
71 instances, coercions and auxiliary constants left out.

Tactic trace: 33 steps
Open to load the checked before-and-after goal states.
```
lemma sum_inter_card_eq_sum_degree_sq
    {W : Type*} [Fintype W] [DecidableEq W]
    (G : SimpleGraph W) [DecidableRel G.Adj] :
    ∑ p : W × W,
        (((G.neighborFinset p.1) ∩ (G.neighborFinset p.2)).card : ℝ) =
      ∑ a : W, ((G.degree a : ℝ)) ^ 2 := by
…
```
theorem SidorenkoConjecture.sidorenko_K22 Case H = K_{2,2} (four-cycle, also called C_4): Sidorenko's conjecture holds, by Cauchy–Schwarz line 521 source
Source documentation
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].
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, DecidableRel, SimpleGraph.Adj, LE.le, Real, HPow.hPow, Nat, SimpleGraph.homDensity, Fin, OfNat.ofNat, SimpleGraph.completeGraph, Finset.card, Sym2, Sum, SimpleGraph.edgeFinset, completeBipartiteGraph, Classical.propDecidable
Proof uses: Eq.mpr, id, Eq, congrArg, SidorenkoConjecture.edgeCount_completeBipartiteGraph_fin_two, dite, IsEmpty, Fintype.card, Fintype.card_eq_zero, HDiv.hDiv, SimpleGraph.homCount, HMul.hMul, congrFun', Eq.trans, Fintype.card_fin, pow_succ, HAdd.hAdd, pow_zero, one_mul, of_decide_eq_true and 142 more
166 instances, coercions and auxiliary constants left out.

Tactic trace: 76 steps
Open to load the checked before-and-after goal states.
```
theorem sidorenko_K22 {W : Type} [Fintype W] [DecidableEq W]
    (G : SimpleGraph W) [DecidableRel G.Adj] :
    homDensity (completeGraph (Fin 2)) G ^
      ((completeBipartiteGraph (Fin 2) (Fin 2)).edgeFinset.card) ≤
      homDensity (completeBipartiteGraph (Fin 2) (Fin 2)) G := by
…
```
theorem SidorenkoConjecture.sidorenko_K22_both_sides_bounded Consequence of homDensity_le_one: both sides of the Sidorenko K_{2,2} inequality are bounded above by 1 line 637 source
Source documentation
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.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, Nonempty, DecidableEq, SimpleGraph, DecidableRel, SimpleGraph.Adj, And, LE.le, Real, SimpleGraph.homDensity, Fin, OfNat.ofNat, Nat, SimpleGraph.completeGraph, Sum, completeBipartiteGraph, Classical.propDecidable
Proof uses: And.intro, SimpleGraph.homDensity_le_one
18 instances, coercions and auxiliary constants left out.
```
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 :=
…
```
lemma SidorenkoConjecture.edgeCount_eq_zero_of_subsingleton If the domain of H has at most one vertex, H has no edges line 650 source
Source documentation
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.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, Subsingleton, SimpleGraph, DecidableRel, SimpleGraph.Adj, Eq, Nat, Finset.card, Sym2, SimpleGraph.edgeFinset, OfNat.ofNat
Proof uses: Eq.mpr, Finset, EmptyCollection.emptyCollection, id, congrArg, propext, Finset.card_eq_zero, Not, Membership.mem, Finset.eq_empty_iff_forall_notMem, Sym2.ind, Set, SimpleGraph.edgeSet, False, Sym2.mk, SimpleGraph.ne_of_adj, Eq.mp, SimpleGraph.mem_edgeSet, Subsingleton.elim, SimpleGraph.mem_edgeFinset
10 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
lemma edgeCount_eq_zero_of_subsingleton {V : Type*} [Fintype V] [Subsingleton V]
    (H : SimpleGraph V) [DecidableRel H.Adj] : H.edgeFinset.card = 0 := by
…
```
lemma SidorenkoConjecture.homCount_eq_of_subsingleton If the domain of H has at most one vertex, every function V → W is a homomorphism H →g G line 668 source
Source documentation
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.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, Subsingleton, DecidableEq, SimpleGraph, DecidableRel, SimpleGraph.Adj, Eq, Nat, SimpleGraph.homCount, HPow.hPow, Fintype.card
Proof uses: id, Eq.mpr, SimpleGraph.Hom, congrArg, Eq.symm, Fintype.card_fun, Fintype.card_congr, Equiv.mk, RelHom.mk, False.elim, SimpleGraph.ne_of_adj, Subsingleton.elim, rfl
12 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma homCount_eq_of_subsingleton {V W : Type*} [Fintype V] [Fintype W]
    [Subsingleton V] [DecidableEq V] [DecidableEq W]
    (H : SimpleGraph V) (G : SimpleGraph W)
    [DecidableRel H.Adj] [DecidableRel G.Adj] :
    homCount H G = (Fintype.card W) ^ (Fintype.card V) := by
…
```
theorem SidorenkoConjecture.sidorenko_tree_subsingleton Base case of Sidorenko for trees line 690 source
Source documentation
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.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, Subsingleton, DecidableEq, Nonempty, SimpleGraph, DecidableRel, SimpleGraph.Adj, LE.le, Real, HPow.hPow, Nat, SimpleGraph.homDensity, Fin, OfNat.ofNat, SimpleGraph.completeGraph, Finset.card, Sym2, SimpleGraph.edgeFinset
Proof uses: Eq.mpr, id, Eq, congrArg, SidorenkoConjecture.edgeCount_eq_zero_of_subsingleton, pow_zero, LT.lt, Fintype.card, Fintype.card_pos, pow_pos, cast, Eq.symm, Eq.trans, congrFun', Nat.cast_zero, HDiv.hDiv, SimpleGraph.homCount, SimpleGraph.homDensity.eq_1, SidorenkoConjecture.homCount_eq_of_subsingleton, Nat.cast_pow and 3 more
79 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
theorem sidorenko_tree_subsingleton {V W : Type} [Fintype V] [Fintype W]
    [Subsingleton V] [DecidableEq V] [DecidableEq W] [Nonempty W]
    (H : SimpleGraph V) (G : SimpleGraph W)
    [DecidableRel H.Adj] [DecidableRel G.Adj] :
    homDensity (completeGraph (Fin 2)) G ^ (H.edgeFinset.card) ≤ homDensity H G := by
…
```
theorem SidorenkoConjecture.sidorenko_tree Case: H is a tree (Sidorenko 1993) sorry line 723 source
Source documentation
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.
depends on sorry what this means
Statement uses: Fintype, DecidableEq, Nonempty, SimpleGraph, DecidableRel, SimpleGraph.Adj, SimpleGraph.IsTree, LE.le, Real, HPow.hPow, Nat, SimpleGraph.homDensity, Fin, OfNat.ofNat, SimpleGraph.completeGraph, Finset.card, Sym2, SimpleGraph.edgeFinset
Proof uses: SimpleGraph.Connected.nonempty, SimpleGraph.IsTree.connected, dite, Subsingleton, Classical.propDecidable, SidorenkoConjecture.sidorenko_tree_subsingleton, Not, sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
22 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
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 := by
…
```
theorem SidorenkoConjecture.sidorenko_conjecture.variants.complete_bipartite Case: complete bipartite graphs K_{s,t} (Sidorenko 1993) sorry line 762 source
Source documentation
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].

depends on sorry what this means
Statement uses: Nat, DecidableRel, Sum, Fin, SimpleGraph.Adj, completeBipartiteGraph, Fintype, DecidableEq, Nonempty, SimpleGraph, LE.le, Real, HPow.hPow, SimpleGraph.homDensity, OfNat.ofNat, SimpleGraph.completeGraph, Finset.card, Sym2, SimpleGraph.edgeFinset
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
26 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
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 := by
…
```
theorem SidorenkoConjecture.sidorenko_conjecture.variants.even_cycle Case: even cycles C_{2k} (Sidorenko 1993) sorry line 781 source
Source documentation
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].

depends on sorry what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Fintype, DecidableEq, Nonempty, SimpleGraph, DecidableRel, SimpleGraph.Adj, Real, HPow.hPow, SimpleGraph.homDensity, Fin, SimpleGraph.completeGraph, Finset.card, Sym2, HMul.hMul, SimpleGraph.edgeFinset, SimpleGraph.cycleGraph
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
30 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
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 := by
…
```
theorem SidorenkoConjecture.sidorenko_conjecture.variants.path_blakley_roy Case: paths, the Blakley–Roy inequality (1965) sorry line 800 source
Source documentation
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].

depends on sorry what this means
Statement uses: Nat, DecidableRel, Fin, SimpleGraph.Adj, SimpleGraph.pathGraph, Fintype, DecidableEq, Nonempty, SimpleGraph, LE.le, Real, HPow.hPow, SimpleGraph.homDensity, OfNat.ofNat, SimpleGraph.completeGraph, Finset.card, Sym2, SimpleGraph.edgeFinset
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
22 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
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 := by
…
```
lemma SidorenkoConjecture.homCount_star_eq_sum_degree_pow Homomorphism count of the star K_{1,m} line 816 source
Source documentation
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.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, DecidableRel, Sum, Fin, OfNat.ofNat, SimpleGraph.Adj, completeBipartiteGraph, Fintype, DecidableEq, SimpleGraph, Eq, SimpleGraph.homCount, Finset.sum, Finset.univ, HPow.hPow, SimpleGraph.degree, Membership.mem, Set, SimpleGraph.neighborSet
Proof uses: id, Equiv, SimpleGraph.Hom, Sigma, Subtype, Finset, SimpleGraph.neighborFinset, Equiv.mk, Sigma.mk, Sum.inl, Subtype.mk, Sum.inr, Eq.mpr, congrArg, propext, SimpleGraph.mem_neighborFinset, SimpleGraph.Hom.map_adj, of_eq_true, Or, And and 37 more
41 instances, coercions and auxiliary constants left out.

Tactic trace: 35 steps
Open to load the checked before-and-after goal states.
```
lemma homCount_star_eq_sum_degree_pow (m : ℕ)
    [DecidableRel (completeBipartiteGraph (Fin 1) (Fin m)).Adj]
    {W : Type*} [Fintype W] [DecidableEq W]
    (G : SimpleGraph W) [DecidableRel G.Adj] :
    homCount (completeBipartiteGraph (Fin 1) (Fin m)) G = ∑ c : W, (G.degree c) ^ m := by
…
```
Mentions: c
lemma SidorenkoConjecture.card_edgeFinset_star Edge count of the star K_{1,m} line 872 source
Source documentation
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).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, DecidableRel, Sum, Fin, OfNat.ofNat, SimpleGraph.Adj, completeBipartiteGraph, Eq, Finset.card, Sym2, SimpleGraph.edgeFinset
Proof uses: SimpleGraph.degree, Sum.inl, Membership.mem, Set, SimpleGraph.neighborSet, Eq.mpr, SimpleGraph.neighborFinset, id, congrArg, Eq.symm, SimpleGraph.card_neighborFinset_eq_degree, Finset.filter, Finset.univ, Finset, SimpleGraph.neighborFinset_eq_filter, Finset.map, Function.Embedding.mk, Sum.inr, Sum.inr_injective, Finset.ext and 71 more
59 instances, coercions and auxiliary constants left out.

Tactic trace: 28 steps
Open to load the checked before-and-after goal states.
```
lemma card_edgeFinset_star (m : ℕ)
    [DecidableRel (completeBipartiteGraph (Fin 1) (Fin m)).Adj] :
    (completeBipartiteGraph (Fin 1) (Fin m)).edgeFinset.card = m := by
…
```
theorem SidorenkoConjecture.sidorenko_conjecture.variants.star Case: stars K_{1,m} (Sidorenko) line 919 source
Source documentation
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.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, DecidableRel, Sum, Fin, OfNat.ofNat, SimpleGraph.Adj, completeBipartiteGraph, Fintype, DecidableEq, Nonempty, SimpleGraph, LE.le, Real, HPow.hPow, SimpleGraph.homDensity, SimpleGraph.completeGraph, Finset.card, Sym2, SimpleGraph.edgeFinset
Proof uses: Eq.mpr, id, Eq, congrArg, SidorenkoConjecture.card_edgeFinset_star, Fintype.card, rfl, LT.lt, cast, Eq.symm, Eq.trans, congrFun', Nat.cast_zero, Fintype.card_pos, HDiv.hDiv, Finset.sum, Finset.univ, SimpleGraph.degree, Membership.mem, Set and 93 more
158 instances, coercions and auxiliary constants left out.

Tactic trace: 35 steps
Open to load the checked before-and-after goal states.
```
theorem sidorenko_conjecture.variants.star (m : ℕ)
    [DecidableRel (completeBipartiteGraph (Fin 1) (Fin m)).Adj]
    {W : Type} [Fintype W] [DecidableEq W] [Nonempty W]
    (G : SimpleGraph W) [DecidableRel G.Adj] :
    homDensity (completeGraph (Fin 2)) G ^
        ((completeBipartiteGraph (Fin 1) (Fin m)).edgeFinset.card) ≤
      homDensity (completeBipartiteGraph (Fin 1) (Fin m)) G := by
…
```
theorem SidorenkoConjecture.sidorenko_conjecture.variants.non_bipartite_necessary Bipartiteness is necessary: the triangle is not a Sidorenko graph line 978 source
Source documentation
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)}.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: LT.lt, Real, SimpleGraph.homDensity, Fin, OfNat.ofNat, Nat, SimpleGraph.completeGraph, HPow.hPow, Finset.card, Sym2, SimpleGraph.edgeFinset
Proof uses: Eq, Eq.mpr, Nat.choose, id, congrArg, SimpleGraph.card_edgeFinset_completeGraph_fin, of_decide_eq_true, Bool, Decidable.decide, Bool.true, Eq.refl, HDiv.hDiv, SimpleGraph.homCount, Fintype.card, HMul.hMul, SidorenkoConjecture.homCount_completeGraph_fin_two_eq_two_mul_card_edgeFinset, congrFun', congr, Nat.choose_self, Fintype.card_fin and 45 more
80 instances, coercions and auxiliary constants left out.

Tactic trace: 30 steps
Open to load the checked before-and-after goal states.
```
theorem sidorenko_conjecture.variants.non_bipartite_necessary :
    homDensity (completeGraph (Fin 3)) (completeGraph (Fin 2)) <
      homDensity (completeGraph (Fin 2)) (completeGraph (Fin 2)) ^
        ((completeGraph (Fin 3)).edgeFinset.card) := by
…
```