Caro-Wei / Turan Graph Pruning Retention Positivity
Provedgraph_independent_set_retention_positivecombinatoricserdos-problemsnumber-theory
For any conflict graph on V vertices with average degree k >= 0, the Turan independent set size V / (k+1) is strictly positive and bounded by V.
Formal statement
import Mathlib
theorem graph_independent_set_retention_positive (V_size : ℝ) (k : ℝ) (hV : 0 < V_size) (hk : 0 ≤ k) :
0 < V_size / (k + 1) ∧ V_size / (k + 1) ≤ V_size := by sorry