structure GalvinTetali.LoopGraph (W : Type u_1) : Type u_1

A LoopGraph on a vertex set $W$: a symmetric relation Adj on $W$, allowing self-loops (unlike SimpleGraph). Used as the target graph $H$ in graph homomorphism counts.

• Adj : W → W → Prop
• symm (u v : W) : self.Adj u v → self.Adj v u

def GalvinTetali.IsGraphHom {V : Type u_1} {W : Type u_2} (G : SimpleGraph V) (H : LoopGraph W) (φ : V → W) : Prop

IsGraphHom G H φ says that $\varphi : V \to W$ is a graph homomorphism from the simple graph $G$ on $V$ to the loop graph $H$ on $W$: adjacent vertices map to adjacent vertices.

noncomputable def GalvinTetali.homCount {V : Type u_1} {W : Type u_2} [Fintype V] [Fintype W] (G : SimpleGraph V) (H : LoopGraph W) : ℕ

The number $\mathrm{hom}(G, H)$ of graph homomorphisms from a finite simple graph $G$ to a finite loop graph $H$.

theorem GalvinTetali.galvin_tetali {V : Type u_1} {W : Type u_2} [Fintype V] [Fintype W] (G : SimpleGraph V) (H : LoopGraph W) (d : ℕ) (hd : 0 < d) (hreg : G.IsRegularOfDegree d) (hbip : G.IsBipartite) : ↑(homCount G H) ≤ ↑(homCount (completeBipartiteGraph (Fin d) (Fin d)) H) ^ (↑(Fintype.card V) / (2 * ↑d))

Theorem 10.4.14 (Galvin–Tetali 2004). For every bipartite $d$-regular graph $G$ on $n$ vertices and any loop graph $H$, $\mathrm{hom}(G, H) \le \mathrm{hom}(K_{d,d}, H)^{n/(2d)}$.