Documentation

Mathlib.Combinatorics.SimpleGraph.Extremal.Basic

Extremal graph theory #

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

Main definitions #

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

Equations
Instances For
    theorem SimpleGraph.IsExtremal.prop {V : Type u_1} [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] {p : SimpleGraph VProp} (h : G.IsExtremal p) :
    p G
    theorem SimpleGraph.exists_isExtremal_iff_exists {V : Type u_1} [Fintype V] (p : SimpleGraph VProp) :
    (∃ (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.

    Equations
    Instances For
      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

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

      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 GG.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 : ) :

      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 GG.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) :

      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₂) :

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

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