Written on the Wall II - Conjecture 20

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

theorem WrittenOnTheWallII.GraphConjecture20.conjecture20 {α : Type u_1} [Fintype α] [DecidableEq α] [Nontrivial α] (G : SimpleGraph α) [DecidableRel G.Adj] (h : G.Connected) : have deg_avg := (∑ v : α, ↑(G.degree v)) / ↑(Fintype.card α); G.n / ↑⌊deg_avg⌋ ≤ G.b

WOWII Conjecture 20

For a simple connected graph G, b(G) ≥ n(G) / ⌊deg_avg(G)⌋, where b(G) is the size of a largest induced bipartite subgraph, n(G) is the number of vertices, and deg_avg(G) = (∑ v, deg(v)) / n(G) is the average degree.