Written on the Wall II - Conjecture 103

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

theorem WrittenOnTheWallII.GraphConjecture103.conjecture103 {α : Type u_1} [Fintype α] [DecidableEq α] [Nontrivial α] (G : SimpleGraph α) (h : G.Connected) : ↑G.indepNum ≤ ↑⌊G.b - Real.log G.averageEccentricity⌋

WOWII Conjecture 103

For a simple connected graph $G$, $\alpha(G) \le \lfloor b(G) - \ln(\mathrm{ecc\_avg}(G)) \rfloor$ where $\alpha(G) = G.\mathrm{indepNum}$ is the independence number, $b(G)$ is the largest induced bipartite subgraph size, and $\mathrm{ecc\_avg}(G) = G.\mathrm{averageEccentricity}$ is the average eccentricity of $G$. Uses Real.log (natural logarithm).