theorem SimpleGraph.exists_indepSet_of_sum_le {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (S : Finset V) : ∃ I ⊆ S, G.IsIndepSet ↑I ∧ ∑ v ∈ S, 1 / (↑(G.degree v) + 1) ≤ ↑I.card

Restricted Caro–Wei: for any finite set of vertices $S$ there is an independent set $I \subseteq S$ with $|I| \geq \sum_{v \in S} 1/(d_v + 1)$. Proved by the standard greedy/induction argument removing a minimum-degree vertex and its neighborhood.

theorem SimpleGraph.caro_wei {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : ∃ (I : Finset V), G.IsIndepSet ↑I ∧ ∑ v : V, 1 / (↑(G.degree v) + 1) ≤ ↑I.card

Caro–Wei theorem (Theorem 2.3.2, Caro 1979 / Wei 1981). Every finite graph $G$ contains an independent set of size at least $\sum_{v \in V} \frac{1}{d_v + 1}$.

theorem SimpleGraph.sum_compl_deg_eq {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : ∑ v : V, 1 / (↑(Gᶜ.degree v) + 1) = ∑ v : V, 1 / (↑(Fintype.card V) - ↑(G.degree v))

Rewriting the Caro–Wei sum on the complement graph in terms of $G$: using $d_{\overline G}(v) + 1 = |V| - d_G(v)$.

theorem SimpleGraph.caro_wei_clique {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : ∃ (C : Finset V), G.IsClique ↑C ∧ ∑ v : V, 1 / (↑(Fintype.card V) - ↑(G.degree v)) ≤ ↑C.card

Caro–Wei for cliques (Corollary 2.3.5). Every finite graph $G$ contains a clique of size at least $\sum_{v \in V} \frac{1}{|V| - d_v}$, obtained by applying Caro–Wei to the complement graph.