Written on the Wall II - Conjecture 2

Reference: E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc

theorem WrittenOnTheWallII.GraphConjecture2.conjecture2 {α : Type u_1} [Fintype α] [DecidableEq α] [Nontrivial α] (G : SimpleGraph α) (h : G.Connected) : 2 * (G.averageIndepNeighbors - 1) ≤ G.Ls

WOWII Conjecture 2

For a simple connected graph G, Ls(G) ≥ 2 · (l(G) - 1) where l(G) is the average independence number of the neighbourhoods of the vertices of G.