Documentation

FormalConjectures.WrittenOnTheWallII.GraphConjecture19

Written on the Wall II - Conjecture 19 #

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

theorem WrittenOnTheWallII.GraphConjecture19.conjecture19 {α : Type u_1} [Fintype α] [DecidableEq α] (G : SimpleGraph α) [Nontrivial α] (h_conn : G.Connected) :
(∑ v : α, (G.eccentricity v).toNat) / (Fintype.card α) + sSup (Set.range G.indepNeighbors) G.b

WOWII Conjecture 19

If G is connected then the size b(G) of a largest induced bipartite subgraph satisfies b(G) ≥ FLOOR((∑ ecc(v))/(|V|) + sSup (range (l G))), where ecc(v) denotes eccentricity and l(G) is the independence number of neighbourhoods.