@[implicit_reducible]

instance SimpleGraph.completeBipartiteGraph.instDecidableRel (V : Type u_1) (W : Type u_2) [DecidableEq V] [DecidableEq W] : DecidableRel (completeBipartiteGraph V W).Adj

Decidability of adjacency in the complete bipartite graph on $V \sqcup W$.

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

$i(G)$: the number of independent sets in a finite simple graph $G$, counting the empty set.

theorem SimpleGraph.numIndSets_completeBipartiteGraph (d : ℕ) (hd : 0 < d) : (completeBipartiteGraph (Fin d) (Fin d)).numIndSets = 2 ^ (d + 1) - 1

The number of independent sets in $K_{d, d}$ equals $2^{d+1} - 1$: a nonempty independent set is any nonempty subset of either side.

theorem SimpleGraph.numIndSets_sq_le_numIndSets_bipartiteDoubleCover {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : ↑G.numIndSets ^ 2 ≤ ↑G.bipartiteDoubleCover.numIndSets

The independent-set count of $G$ squared is at most that of its bipartite double cover $G \times K_2$: $i(G)^2 \leq i(G \times K_2)$.

theorem SimpleGraph.kahn_zhao_bipartite {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (d : ℕ) (hd : 0 < d) (hreg : G.IsRegularOfDegree d) (hbip : G.IsBipartite) : ↑G.numIndSets ≤ ↑(completeBipartiteGraph (Fin d) (Fin d)).numIndSets ^ (↑(Fintype.card V) / (2 * ↑d))

Kahn-Zhao for bipartite graphs (Kahn 2001): for a $d$-regular bipartite graph $G$ on $n$ vertices, $i(G) \leq i(K_{d, d})^{n / (2d)}$.

theorem SimpleGraph.kahn_zhao {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (d : ℕ) (hd : 0 < d) (hreg : G.IsRegularOfDegree d) : ↑G.numIndSets ≤ ↑(completeBipartiteGraph (Fin d) (Fin d)).numIndSets ^ (↑(Fintype.card V) / (2 * ↑d))

Theorem 10.4.12 (Kahn-Zhao): for any $d$-regular graph $G$ on $n$ vertices, $i(G) \leq i(K_{d, d})^{n / (2d)}$, deduced from the bipartite case via the bipartite double-cover trick.