Extremal graph theory

This file introduces basic definitions for extremal graph theory, including extremal numbers.

Main definitions

• SimpleGraph.IsExtremal is the predicate that G satisfies p and any H satisfying p has at most as many edges as G.

• SimpleGraph.extremalNumber is the maximum number of edges in a H-free simple graph on n vertices.

  If H is contained in all simple graphs on n vertices, then this is 0.

def SimpleGraph.IsExtremal {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (p : SimpleGraph V → Prop) : Prop

G is an extremal graph satisfying p if G has the maximum number of edges of any simple graph satisfying p.

theorem SimpleGraph.IsExtremal.prop {V : Type u_1} [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] {p : SimpleGraph V → Prop} (h : G.IsExtremal p) : p G

theorem SimpleGraph.exists_isExtremal_iff_exists {V : Type u_1} [Fintype V] (p : SimpleGraph V → Prop) : (∃ (G : SimpleGraph V) (x : DecidableRel G.Adj), G.IsExtremal p) ↔ ∃ (G : SimpleGraph V), p G

If one simple graph satisfies p, then there exists an extremal graph satisfying p.

theorem SimpleGraph.exists_isExtremal_free {V : Type u_1} [Fintype V] {W : Type u_2} {H : SimpleGraph W} (h : H ≠ ⊥) : ∃ (G : SimpleGraph V) (x : DecidableRel G.Adj), G.IsExtremal H.Free

If H has at least one edge, then there exists an extremal H.Free graph.

noncomputable def SimpleGraph.extremalNumber (n : ℕ) {W : Type u_1} (H : SimpleGraph W) : ℕ

The extremal number of a natural number n and a simple graph H is the the maximum number of edges in a H-free simple graph on n vertices.

If H is contained in all simple graphs on n vertices, then this is 0.

theorem SimpleGraph.extremalNumber_of_fintypeCard_eq {n : ℕ} {V : Type u_1} {W : Type u_2} {H : SimpleGraph W} [Fintype V] (hc : Fintype.card V = n) : extremalNumber n H = {G : SimpleGraph V | H.Free G}.sup fun (x : SimpleGraph V) => x.edgeFinset.card

theorem SimpleGraph.card_edgeFinset_le_extremalNumber {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} [Fintype V] [DecidableRel G.Adj] (h : H.Free G) : G.edgeFinset.card ≤ extremalNumber (Fintype.card V) H

If G is H-free, then G has at most extremalNumber (card V) H edges.

theorem SimpleGraph.IsContained.of_extremalNumber_lt_card_edgeFinset {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} [Fintype V] [DecidableRel G.Adj] (h : extremalNumber (Fintype.card V) H < G.edgeFinset.card) : H.IsContained G

If G has more than extremalNumber (card V) H edges, then G contains a copy of H.

theorem SimpleGraph.extremalNumber_le_iff {V : Type u_1} {W : Type u_2} [Fintype V] (H : SimpleGraph W) (m : ℕ) : extremalNumber (Fintype.card V) H ≤ m ↔ ∀ ⦃G : SimpleGraph V⦄ [inst : DecidableRel G.Adj], H.Free G → G.edgeFinset.card ≤ m

extremalNumber (card V) H is at most x if and only if every H-free simple graph G has at most x edges.

theorem SimpleGraph.lt_extremalNumber_iff {V : Type u_1} {W : Type u_2} [Fintype V] (H : SimpleGraph W) (m : ℕ) : m < extremalNumber (Fintype.card V) H ↔ ∃ (G : SimpleGraph V) (x : DecidableRel G.Adj), H.Free G ∧ m < G.edgeFinset.card

extremalNumber (card V) H is greater than x if and only if there exists a H-free simple graph G with more than x edges.

theorem SimpleGraph.extremalNumber_le_iff_of_nonneg {V : Type u_1} {W : Type u_2} [Fintype V] {R : Type u_3} [Semiring R] [LinearOrder R] [FloorSemiring R] (H : SimpleGraph W) {m : R} (h : 0 ≤ m) : ↑(extremalNumber (Fintype.card V) H) ≤ m ↔ ∀ ⦃G : SimpleGraph V⦄ [inst : DecidableRel G.Adj], H.Free G → ↑G.edgeFinset.card ≤ m

extremalNumber (card V) H is at most x if and only if every H-free simple graph G has at most x edges.

theorem SimpleGraph.lt_extremalNumber_iff_of_nonneg {V : Type u_1} {W : Type u_2} [Fintype V] {R : Type u_3} [Semiring R] [LinearOrder R] [FloorSemiring R] (H : SimpleGraph W) {m : R} (h : 0 ≤ m) : m < ↑(extremalNumber (Fintype.card V) H) ↔ ∃ (G : SimpleGraph V) (x : DecidableRel G.Adj), H.Free G ∧ m < ↑G.edgeFinset.card

extremalNumber (card V) H is greater than x if and only if there exists a H-free simple graph G with more than x edges.

theorem SimpleGraph.IsContained.extremalNumber_le {n : ℕ} {W : Type u_2} {H : SimpleGraph W} {W' : Type u_4} {H' : SimpleGraph W'} (h : H'.IsContained H) : extremalNumber n H' ≤ extremalNumber n H

If H contains a copy of H', then extremalNumber n H is at most extremalNumber n H.

theorem SimpleGraph.extremalNumber_congr {n₁ n₂ : ℕ} {W₁ : Type u_4} {W₂ : Type u_5} {H₁ : SimpleGraph W₁} {H₂ : SimpleGraph W₂} (h : n₁ = n₂) (e : H₁ ≃g H₂) : extremalNumber n₁ H₁ = extremalNumber n₂ H₂

If H₁ ≃g H₂, then extremalNumber n H₁ equals extremalNumber n H₂.

theorem SimpleGraph.extremalNumber_congr_right {n : ℕ} {W₁ : Type u_4} {W₂ : Type u_5} {H₁ : SimpleGraph W₁} {H₂ : SimpleGraph W₂} (e : H₁ ≃g H₂) : extremalNumber n H₁ = extremalNumber n H₂

If H₁ ≃g H₂, then extremalNumber n H₁ equals extremalNumber n H₂.

theorem SimpleGraph.isExtremal_free_iff {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} [Fintype V] [DecidableRel G.Adj] : G.IsExtremal H.Free ↔ H.Free G ∧ G.edgeFinset.card = extremalNumber (Fintype.card V) H

H-free extremal graphs are H-free simple graphs having extremalNumber (card V) H many edges.

theorem SimpleGraph.card_edgeFinset_of_isExtremal_free {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} [Fintype V] [DecidableRel G.Adj] (h : G.IsExtremal H.Free) : G.edgeFinset.card = extremalNumber (Fintype.card V) H

theorem SimpleGraph.card_edgeFinset_deleteIncidenceSet_le_extremalNumber {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} [Fintype V] [DecidableRel G.Adj] [DecidableEq V] (h : H.Free G) (v : V) : (G.deleteIncidenceSet v).edgeFinset.card ≤ extremalNumber (Fintype.card V - 1) H

If G is H.Free, then G.deleteIncidenceSet v is also H.Free and has at most extremalNumber (card V-1) H many edges.