Size Ramsey Number #
This file defines the size Ramsey number for simple graphs.
Definition #
The size Ramsey number r̂(G, H) is the minimum number of edges in a graph F
such that any 2-coloring of F's edges contains a copy of G in one color or H in the other.
noncomputable def
SimpleGraph.sizeRamsey
{α : Type u_1}
{β : Type u_2}
[Fintype α]
[Fintype β]
(G : SimpleGraph α)
(H : SimpleGraph β)
:
The size Ramsey number r̂(G, H) is the minimum number of edges in a graph F
such that any 2-coloring of F's edges contains a copy of G in one color or H in the other.
A 2-coloring is represented by a subgraph R ≤ F (the "red" edges); the "blue" edges are F \ R.
Equations
- G.sizeRamsey H = sInf {m : ℕ | ∃ (n : ℕ) (F : SimpleGraph (Fin n)), F.edgeSet.ncard = m ∧ ∀ R ≤ F, G.IsContained R ∨ H.IsContained (F \ R)}
Instances For
A graph G is Ramsey size linear if there exists a constant c > 0 such that
for all graphs H with m edges and no isolated vertices, r̂(G, H) ≤ c · m.
Equations
- G.IsRamseySizeLinear = ∃ c > 0, ∀ (n : ℕ) (H : SimpleGraph (Fin n)) [inst : DecidableRel H.Adj], (∀ (v : Fin n), 0 < H.degree v) → ↑(G.sizeRamsey H) ≤ c * ↑H.edgeSet.ncard