Extremal graph theory #
This file introduces basic definitions for extremal graph theory, including extremal numbers.
Main definitions #
SimpleGraph.IsExtremal
is the predicate thatG
satisfiesp
and anyH
satisfyingp
has at most as many edges asG
.SimpleGraph.extremalNumber
is the maximum number of edges in aH
-free simple graph onn
vertices.If
H
is contained in all simple graphs onn
vertices, then this is0
.
G
is an extremal graph satisfying p
if G
has the maximum number of edges of any simple
graph satisfying p
.
Equations
- G.IsExtremal p = (p G ∧ ∀ ⦃G' : SimpleGraph V⦄ [inst : DecidableRel G'.Adj], p G' → G'.edgeFinset.card ≤ G.edgeFinset.card)
Instances For
If one simple graph satisfies p
, then there exists an extremal graph satisfying p
.
If H
has at least one edge, then there exists an extremal H.Free
graph.
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
- SimpleGraph.extremalNumber n H = {G : SimpleGraph (Fin n) | H.Free G}.sup fun (x : SimpleGraph (Fin n)) => x.edgeFinset.card
Instances For
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
.
extremalNumber (card V) H
is at most x
if and only if every H
-free simple graph G
has
at most x
edges.
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.
extremalNumber (card V) H
is at most x
if and only if every H
-free simple graph G
has
at most x
edges.
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.
If H
contains a copy of H'
, then extremalNumber n H
is at most extremalNumber n H
.
If H₁ ≃g H₂
, then extremalNumber n H₁
equals extremalNumber n 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.