def DominatingSet.IsDominatingSet {V : Type u_1} (G : SimpleGraph V) [DecidableRel G.Adj] (D : Finset V) : Prop

A set $D \subseteq V$ is a dominating set of $G$ if every vertex outside $D$ has a neighbor in $D$.

theorem DominatingSet.exists_dominating_from_subset {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (S : Finset V) (hδ : 1 ≤ G.minDegree) : ∃ (D : Finset V), IsDominatingSet G D ∧ D.card ≤ S.card + {v : V | v ∉ S ∧ ∀ u ∈ G.neighborFinset v, u ∉ S}.card

Given any subset $S \subseteq V$, augmenting it with the vertices $Y$ that are neither in $S$ nor adjacent to $S$ produces a dominating set of size at most $|S| + |Y|$.

noncomputable def DominatingSet.bernoulliWeight {V : Type u_1} [Fintype V] (p : ℝ) (S : Finset V) : ℝ

The Bernoulli probability weight of a subset $S \subseteq V$ under independent inclusion with parameter $p$: equals $p^{|S|} (1-p)^{n-|S|}$ where $n = |V|$.

theorem DominatingSet.bernoulliWeight_total {V : Type u_1} [Fintype V] [DecidableEq V] (p : ℝ) : ∑ S ∈ Finset.univ.powerset, bernoulliWeight p S = 1

The Bernoulli weights sum to $1$ over all subsets of $V$, expressing that the random subset distribution is a probability measure.

theorem DominatingSet.bernoulliWeight_expected_cost_le {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (p : ℝ) (hp_pos : 0 < p) (hp_lt_one : p < 1) (hδ : 1 ≤ G.minDegree) : ∑ S ∈ Finset.univ.powerset, bernoulliWeight p S * (↑S.card + ↑{v : V | v ∉ S ∧ ∀ u ∈ G.neighborFinset v, u ∉ S}.card) ≤ ↑(Fintype.card V) * p + ↑(Fintype.card V) * (1 - p) ^ (G.minDegree + 1)

The expected cost $|S| + |Y(S)|$ under the Bernoulli($p$) distribution is bounded by $np + n(1-p)^{\delta + 1}$, where $\delta$ is the minimum degree of $G$.

theorem DominatingSet.exists_dominating_set_bound {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Nonempty V] (hδ : 1 ≤ G.minDegree) : ∃ (D : Finset V), IsDominatingSet G D ∧ ↑D.card ≤ ↑(Fintype.card V) * (1 + Real.log (↑G.minDegree + 1)) / (↑G.minDegree + 1)

Theorem 3.1.1. Every graph $G$ on $n$ vertices with minimum degree $\delta \geq 1$ has a dominating set of size at most $\frac{n(1 + \log(\delta + 1))}{\delta + 1}$.