noncomputable def Sidorenko.homDensity {V : Type u_1} {W : Type u_2} (F : SimpleGraph V) (G : SimpleGraph W) : ℝ

The homomorphism density $t(F,G) = \mathrm{hom}(F,G) / |W|^{|V|}$ of a graph homomorphism from $F$ into $G$, where $V = V(F)$ and $W = V(G)$.

theorem sidorenko_conjecture {V : Type u_1} {W : Type u_2} [Fintype V] [Fintype W] (F : SimpleGraph V) (G : SimpleGraph W) [DecidableRel F.Adj] [DecidableRel G.Adj] (hF : F.IsBipartite) : Sidorenko.homDensity F G ≥ Sidorenko.homDensity ⊤ G ^ F.edgeFinset.card

The Sidorenko conjecture (Conjecture 10.3.2): for any bipartite graph $F$ and any graph $G$, the homomorphism density satisfies $t(F,G) \ge t(K_2,G)^{e(F)}$.

@[implicit_reducible]

instance BlakleyRoy.pathGraph4_decidableAdj : DecidableRel (SimpleGraph.pathGraph 4).Adj

Decidability of adjacency in the path graph $P_4$ on four vertices.

theorem BlakleyRoy.pathGraph4_adj_cases {x y : Fin 4} (h : (SimpleGraph.pathGraph 4).Adj x y) : x = 0 ∧ y = 1 ∨ x = 1 ∧ y = 0 ∨ x = 1 ∧ y = 2 ∨ x = 2 ∧ y = 1 ∨ x = 2 ∧ y = 3 ∨ x = 3 ∧ y = 2

Case analysis on adjacency in the path graph $P_4$: the only adjacent pairs are $(0,1), (1,2), (2,3)$ and their reverses.

noncomputable def BlakleyRoy.walkCount {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : ℕ

Number of length-3 walks in $G$ counted as $\sum_b \deg(b) \sum_{c \sim b} \deg(c)$, used to express homomorphism counts from $P_4$ into $G$.

theorem BlakleyRoy.nat_card_hom_eq_walkCount {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : Nat.card (SimpleGraph.pathGraph 4 →g G) = walkCount G

The number of graph homomorphisms $P_4 \to G$ equals the walk count $\sum_b \deg(b) \sum_{c \sim b} \deg(c)$.

theorem BlakleyRoy.sum_deg_mul_sum_sq_le_card_mul_walkCount {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : (∑ v : V, ↑(G.degree v)) * ∑ v : V, ↑(G.degree v) ^ 2 ≤ ↑(Fintype.card V) * ↑(walkCount G)

Cauchy-Schwarz-type bound: $(\sum_v \deg v)(\sum_v \deg^2 v) \le |V| \cdot W(G)$ where $W(G)$ is the walk count. A key step in proving Blakey-Roy for $P_4$.

theorem BlakleyRoy.blakley_roy {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : (∑ v : V, ↑(G.degree v)) ^ 3 ≤ ↑(Fintype.card V) ^ 2 * ↑(Nat.card (SimpleGraph.pathGraph 4 →g G))

The Blakey-Roy inequality (Theorem 10.3.3, Sidorenko for the three-edge path): $(2 e(G))^3 \le |V(G)|^2 \cdot \mathrm{hom}(P_4, G)$.