Conjecture 1.6 #
Reference: arxiv/2107.00295 On independent domination of regular graphs by Eun-Kyung Cho, Ilkyoo Choi, Boram Park
theorem
Arxiv.«2107.00295».independentDominationEven
{V : Type u_1}
[Fintype V]
[DecidableEq V]
(G : SimpleGraph V)
[DecidableRel G.Adj]
(hIso : 0 < G.minDegree)
(hEven : Even G.maxDegree)
:
have D := G.maxDegree;
have i := G.indepDominationNumber;
have n := Fintype.card V;
(D + 2) ^ 2 * i ≤ (D ^ 2 + 4) * n
Conjecture 1.6 (Even case). For a nonempty isolate-free graph $G$ on $n$ vertices, if $D$ is even, then $(D + 2)^2 \cdot i(G) \leq (D^2 + 4) \cdot n$.
theorem
Arxiv.«2107.00295».independentDominationOdd
{V : Type u_1}
[Fintype V]
[DecidableEq V]
(G : SimpleGraph V)
[DecidableRel G.Adj]
(hIso : 0 < G.minDegree)
(hOdd : Odd G.maxDegree)
:
Conjecture 1.6 (Odd case). For a nonempty isolate-free graph $G$ on $n$ vertices, if $D$ is odd, then $(D + 1)(D + 3) \cdot i(G) \leq (D^2 + 3) \cdot n$.