D-Balanced graphs #
SimpleGraph.IsBalanced G D is the condition that the maximum degree of a simple graph $G$ is
at most $D$ times the minimum degree.
def
SimpleGraph.IsBalanced
{V : Type u_1}
[Fintype V]
(G : SimpleGraph V)
(D : ℝ)
[DecidableRel G.Adj]
:
We call a graph $D$-balanced (or $D$-almost-regular) if the maximum degree is at most $D$ times the minimum degree.