A two-degenerate extremal-number counterexample

This file constructs a connected bipartite two-degenerate graph whose extremal number grows faster than every constant multiple of n ^ (3 / 2).

def TwoDegenerateGraphs.IsDegenerate {V : Type u_1} (r : ℕ) (G : SimpleGraph V) : Prop

Every nonempty induced finite subgraph has a vertex of degree at most r.

Equations

• TwoDegenerateGraphs.IsDegenerate r G = ∀ (s : Finset V), s.Nonempty → ∃ v ∈ s, (TwoDegenerateGraphs.neighborsWithin✝ G s v).card ≤ r

@[reducible, inline]

abbrev TwoDegenerateGraphs.IsTwoDegenerate {V : Type u_1} (G : SimpleGraph V) : Prop

A graph is two-degenerate when every nonempty induced finite subgraph has a vertex with at most two neighbors.

Equations

• TwoDegenerateGraphs.IsTwoDegenerate G = TwoDegenerateGraphs.IsDegenerate 2 G

theorem TwoDegenerateGraphs.twoDegenerateExtremalCounterexample : ∃ (q : ℕ) (H : SimpleGraph (Fin q)), H.Connected ∧ H.IsBipartite ∧ IsTwoDegenerate H ∧ (∀ (coloring : H.Coloring (Fin 2)) (side : Fin 2), 2 < {vertex : Fin q | coloring vertex = side}.sup fun (vertex : Fin q) => H.degree vertex) ∧ ∃ (c : ℝ) (ε : ℝ), 0 < c ∧ 0 < ε ∧ ∀ᶠ (n : ℕ) in Filter.atTop, c * ↑n ^ (3 / 2 + ε) ≤ ↑(SimpleGraph.extremalNumber n H)

A bipartite two-degenerate graph whose extremal number grows faster than every constant multiple of n ^ (3 / 2).