Ramsey numbers

Define edge labellings, monochromatic subsets and ramsey numbers, and prove basic properties of these.

def SimpleGraph.EdgeLabelling {V : Type u_1} (G : SimpleGraph V) (K : Type u_5) : Type (max u_1 u_5)

An edge labelling of a simple graph G with labels in type K. Sometimes this is called an edge-colouring, but we reserve that terminology for labellings where incident edges cannot share a label.

Equations

• G.EdgeLabelling K = (↑G.edgeSet → K)

instance SimpleGraph.instFintypeEdgeLabellingOfDecidableEqOfElemSym2EdgeSet {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} [DecidableEq V] [Fintype ↑G.edgeSet] [Fintype K] : Fintype (G.EdgeLabelling K)

Equations

• SimpleGraph.instFintypeEdgeLabellingOfDecidableEqOfElemSym2EdgeSet = Pi.instFintype

instance SimpleGraph.instNonemptyEdgeLabelling {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} [Nonempty K] : Nonempty (G.EdgeLabelling K)

instance SimpleGraph.instInhabitedEdgeLabelling {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} [Inhabited K] : Inhabited (G.EdgeLabelling K)

Equations

• SimpleGraph.instInhabitedEdgeLabelling = Pi.instInhabited

instance SimpleGraph.instSubsingletonEdgeLabelling {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} [Subsingleton K] : Subsingleton (G.EdgeLabelling K)

instance SimpleGraph.instUniqueEdgeLabelling {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} [Unique K] : Unique (G.EdgeLabelling K)

Equations

• SimpleGraph.instUniqueEdgeLabelling = Pi.unique

instance SimpleGraph.EdgeLabelling.uniqueOfSubsingleton {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} [Subsingleton V] : Unique (G.EdgeLabelling K)

Equations

• SimpleGraph.EdgeLabelling.uniqueOfSubsingleton = Pi.uniqueOfIsEmpty fun (a : ↑G.edgeSet) => K

@[reducible, inline]

abbrev SimpleGraph.TopEdgeLabelling (V : Type u_5) (K : Type u_6) : Type (max u_5 u_6)

An edge labelling of the complete graph on V with labels in type K. Sometimes this is called an edge-colouring, but we reserve that terminology for labellings where incident edges cannot share a label.

Equations

• SimpleGraph.TopEdgeLabelling V K = ⊤.EdgeLabelling K

theorem SimpleGraph.card_EdgeLabelling {V : Type u_1} {K : Type u_3} [DecidableEq V] [Fintype V] [Fintype K] : Fintype.card (TopEdgeLabelling V K) = Fintype.card K ^ (Fintype.card V).choose 2

def SimpleGraph.EdgeLabelling.get {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} (C : G.EdgeLabelling K) (x y : V) (h : G.Adj x y) : K

Convenience function to get the colour of the edge x ~ y in the colouring of the complete graph on V.

Equations

• C.get x y h = C ⟨s(x, y), h⟩

theorem SimpleGraph.EdgeLabelling.get_swap {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} {C : G.EdgeLabelling K} (x y : V) (h : G.Adj x y) : C.get y x ⋯ = C.get x y h

theorem SimpleGraph.EdgeLabelling.ext_get {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} {C C' : G.EdgeLabelling K} (h : ∀ (x y : V) (h : G.Adj x y), C.get x y h = C'.get x y h) : C = C'

theorem SimpleGraph.EdgeLabelling.ext_get_iff {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} {C C' : G.EdgeLabelling K} : C = C' ↔ ∀ (x y : V) (h : G.Adj x y), C.get x y h = C'.get x y h

def SimpleGraph.EdgeLabelling.compRight {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} {K' : Type u_4} (C : G.EdgeLabelling K) (f : K → K') : G.EdgeLabelling K'

Compose an edge-labelling with a function on the colour set.

Equations

• C.compRight f = f ∘ C

def SimpleGraph.EdgeLabelling.pullback {V : Type u_1} {V' : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph V'} {K : Type u_3} (C : G.EdgeLabelling K) (f : G' ↪g G) : G'.EdgeLabelling K

Compose an edge-labelling with a graph embedding.

Equations

• C.pullback f = C ∘ ⇑f.mapEdgeSet

@[simp]

theorem SimpleGraph.EdgeLabelling.pullback_apply {V : Type u_1} {V' : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph V'} {K : Type u_3} {C : G.EdgeLabelling K} {f : G' ↪g G} (e : ↑G'.edgeSet) : C.pullback f e = C (f.mapEdgeSet e)

@[simp]

theorem SimpleGraph.EdgeLabelling.pullback_get {V : Type u_1} {V' : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph V'} {K : Type u_3} {C : G.EdgeLabelling K} {f : G' ↪g G} (x y : V') (h : G'.Adj x y) : (C.pullback f).get x y h = C.get (f x) (f y) ⋯

@[simp]

theorem SimpleGraph.EdgeLabelling.compRight_apply {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} {K' : Type u_4} {C : G.EdgeLabelling K} (f : K → K') (e : ↑G.edgeSet) : C.compRight f e = f (C e)

@[simp]

theorem SimpleGraph.EdgeLabelling.compRight_get {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} {K' : Type u_4} {C : G.EdgeLabelling K} (f : K → K') (x y : V) (h : G.Adj x y) : (C.compRight f).get x y h = f (C.get x y h)

def SimpleGraph.EdgeLabelling.mk {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} (f : (x y : V) → G.Adj x y → K) (f_symm : ∀ (x y : V) (H : G.Adj x y), f y x ⋯ = f x y H) : G.EdgeLabelling K

Construct an edge labelling from a symmetric function taking values everywhere except the diagonal.

Equations

• SimpleGraph.EdgeLabelling.mk f f_symm ⟨e, he⟩ = Quotient.hrecOn (motive := fun (x : Sym2 V) => x ∈ G.edgeSet → K) e (fun (xy : V × V) => f xy.1 xy.2) ⋯ he

theorem SimpleGraph.EdgeLabelling.mk_get {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} (f : (x y : V) → G.Adj x y → K) (f_symm : ∀ (x y : V) (H : G.Adj x y), f y x ⋯ = f x y H) (x y : V) (h : G.Adj x y) : (mk f f_symm).get x y h = f x y h

def SimpleGraph.EdgeLabelling.MonochromaticOf {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} (C : G.EdgeLabelling K) (m : Set V) (c : K) : Prop

χ.MonochromaticOf m c says that every edge in m is assigned the colour c by m.

Equations

• C.MonochromaticOf m c = ∀ ⦃x : V⦄, x ∈ m → ∀ ⦃y : V⦄, y ∈ m → ∀ (h : G.Adj x y), C.get x y h = c

theorem SimpleGraph.EdgeLabelling.monochromaticOf_iff_pairwise {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} [DecidableRel G.Adj] (C : G.EdgeLabelling K) {m : Set V} {c : K} : C.MonochromaticOf m c ↔ m.Pairwise fun (x y : V) => ∀ (h : G.Adj x y), C.get x y h = c

def SimpleGraph.EdgeLabelling.labelGraph {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} (C : G.EdgeLabelling K) (k : K) : SimpleGraph V

Given an edge labelling and a choice of label k, construct the graph corresponding to the edges labelled k.

Equations

• C.labelGraph k = SimpleGraph.fromEdgeSet {e : Sym2 V | ∃ (h : e ∈ G.edgeSet), C ⟨e, h⟩ = k}

theorem SimpleGraph.EdgeLabelling.labelGraph_adj {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} {C : G.EdgeLabelling K} {k : K} (x y : V) : (C.labelGraph k).Adj x y ↔ ∃ (H : G.Adj x y), C ⟨s(x, y), H⟩ = k

instance SimpleGraph.EdgeLabelling.instDecidableRelAdjLabelGraphOfDecidableEq {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} [DecidableRel G.Adj] [DecidableEq K] (k : K) {C : G.EdgeLabelling K} : DecidableRel (C.labelGraph k).Adj

Equations

• SimpleGraph.EdgeLabelling.instDecidableRelAdjLabelGraphOfDecidableEq k x✝¹ x✝ = decidable_of_iff' (∃ (H : G.Adj x✝¹ x✝), C ⟨s(x✝¹, x✝), H⟩ = k) ⋯

theorem SimpleGraph.EdgeLabelling.labelGraph_le {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} (C : G.EdgeLabelling K) {k : K} : C.labelGraph k ≤ G

theorem SimpleGraph.EdgeLabelling.pairwiseDisjoint {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} {C : G.EdgeLabelling K} : Set.univ.PairwiseDisjoint C.labelGraph

theorem SimpleGraph.EdgeLabelling.iSup_labelGraph {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} (C : G.EdgeLabelling K) : ⨆ (k : K), C.labelGraph k = G

theorem SimpleGraph.EdgeLabelling.sup_labelGraph {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} [Fintype K] (C : G.EdgeLabelling K) : Finset.univ.sup C.labelGraph = G

@[reducible, inline]

abbrev SimpleGraph.TopEdgeLabelling.pullback {V : Type u_1} {V' : Type u_2} {K : Type u_3} (C : TopEdgeLabelling V K) (f : V' ↪ V) : TopEdgeLabelling V' K

Compose an edge-labelling, by an injection into the vertex type. This must be an injection, else we don't know how to colour x ~ y in the case f x = f y.

Equations

• C.pullback f = SimpleGraph.EdgeLabelling.pullback C { toEmbedding := f, map_rel_iff' := ⋯ }

@[simp]

theorem SimpleGraph.TopEdgeLabelling.monochromaticOf_iff_ne_of_adj {V : Type u_1} {K : Type u_3} (C : TopEdgeLabelling V K) (m : Set V) (c : K) : EdgeLabelling.MonochromaticOf C m c ↔ ∀ ⦃x : V⦄, x ∈ m → ∀ ⦃y : V⦄, y ∈ m → ∀ (h : x ≠ y), EdgeLabelling.get C x y h = c

@[simp]

theorem SimpleGraph.TopEdgeLabelling.labelGraph_adj {V : Type u_1} {K : Type u_3} {C : TopEdgeLabelling V K} {k : K} (x y : V) : (EdgeLabelling.labelGraph C k).Adj x y ↔ ∃ (H : x ≠ y), EdgeLabelling.get C x y H = k

def SimpleGraph.toTopEdgeLabelling {V : Type u_1} (G : SimpleGraph V) [DecidableRel G.Adj] : TopEdgeLabelling V (Fin 2)

From a simple graph on V, construct the edge labelling on the complete graph of V given where edges are labelled 1 and non-edges are labelled 0.

Equations

• G.toTopEdgeLabelling = SimpleGraph.EdgeLabelling.mk (fun (x y : V) (x_1 : ⊤.Adj x y) => if G.Adj x y then 1 else 0) ⋯

@[simp]

theorem SimpleGraph.toTopEdgeLabelling_get {V : Type u_1} {G : SimpleGraph V} [DecidableRel G.Adj] {x y : V} (H : x ≠ y) : EdgeLabelling.get G.toTopEdgeLabelling x y H = if G.Adj x y then 1 else 0

theorem SimpleGraph.toTopEdgeLabelling_labelGraph {V : Type u_1} (G : SimpleGraph V) [DecidableRel G.Adj] : EdgeLabelling.labelGraph G.toTopEdgeLabelling 1 = G

theorem SimpleGraph.toTopEdgeLabelling_labelGraph_compl {V : Type u_1} (G : SimpleGraph V) [DecidableRel G.Adj] : EdgeLabelling.labelGraph G.toTopEdgeLabelling 0 = Gᶜ

theorem SimpleGraph.TopEdgeLabelling.labelGraph_toTopEdgeLabelling {V : Type u_1} [DecidableEq V] (C : TopEdgeLabelling V (Fin 2)) : (EdgeLabelling.labelGraph C 1).toTopEdgeLabelling = C

instance SimpleGraph.instDecidableMonochromaticOfToSetOfDecidableEqOfDecidableRelAdj {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} [DecidableEq K] [DecidableEq V] [DecidableRel G.Adj] (C : G.EdgeLabelling K) (m : Finset V) (c : K) : Decidable (C.MonochromaticOf (↑m) c)

Equations

• SimpleGraph.instDecidableMonochromaticOfToSetOfDecidableEqOfDecidableRelAdj C m c = decidable_of_iff' ((↑m).Pairwise fun (x y : V) => ∀ (h : G.Adj x y), C.get x y h = c) ⋯

@[simp]

theorem SimpleGraph.EdgeLabelling.monochromaticOf_empty {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} {c : K} {C : G.EdgeLabelling K} : C.MonochromaticOf ∅ c

@[simp]

theorem SimpleGraph.EdgeLabelling.monochromaticOf_singleton {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} {c : K} {C : G.EdgeLabelling K} {x : V} : C.MonochromaticOf {x} c

theorem SimpleGraph.EdgeLabelling.monochromatic_finset_singleton {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} {c : K} {C : G.EdgeLabelling K} {x : V} : C.MonochromaticOf (↑{x}) c

theorem SimpleGraph.EdgeLabelling.monochromatic_subsingleton {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} {m : Set V} {c : K} {C : G.EdgeLabelling K} (hm : m.Subsingleton) : C.MonochromaticOf m c

theorem SimpleGraph.EdgeLabelling.monochromatic_subsingleton_colours {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} {m : Set V} {c : K} {C : G.EdgeLabelling K} [Subsingleton K] : C.MonochromaticOf m c

theorem SimpleGraph.EdgeLabelling.MonochromaticOf.compRight {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} {K' : Type u_4} {m : Set V} {c : K} {C : G.EdgeLabelling K} (e : K → K') (h : C.MonochromaticOf m c) : (C.compRight e).MonochromaticOf m (e c)

theorem SimpleGraph.EdgeLabelling.monochromaticOf_injective {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} {K' : Type u_4} {m : Set V} {c : K} {C : G.EdgeLabelling K} (e : K → K') (he : Function.Injective e) : (C.compRight e).MonochromaticOf m (e c) ↔ C.MonochromaticOf m c

theorem SimpleGraph.EdgeLabelling.MonochromaticOf.subset {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} {m : Set V} {c : K} {C : G.EdgeLabelling K} {m' : Set V} (h' : m' ⊆ m) (h : C.MonochromaticOf m c) : C.MonochromaticOf m' c

theorem SimpleGraph.EdgeLabelling.MonochromaticOf.image {V : Type u_1} {V' : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph V'} {K : Type u_3} {m : Set V} {c : K} {C : G'.EdgeLabelling K} {f : G ↪g G'} (h : (C.pullback f).MonochromaticOf m c) : C.MonochromaticOf (⇑f '' m) c

theorem SimpleGraph.EdgeLabelling.MonochromaticOf.map {V : Type u_1} {V' : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph V'} {K : Type u_3} {c : K} {C : G'.EdgeLabelling K} {f : G ↪g G'} {m : Finset V} (h : (C.pullback f).MonochromaticOf (↑m) c) : C.MonochromaticOf (↑(Finset.map f.toEmbedding m)) c

def SimpleGraph.EdgeLabelling.MonochromaticBetween {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} (C : G.EdgeLabelling K) (X Y : Set V) (k : K) : Prop

The predicate χ.MonochromaticBetween X Y k says every edge between X and Y is labelled k by the labelling χ.

Equations

• C.MonochromaticBetween X Y k = ∀ ⦃x : V⦄, x ∈ X → ∀ ⦃y : V⦄, y ∈ Y → ∀ (h : G.Adj x y), C.get x y h = k

instance SimpleGraph.EdgeLabelling.instDecidableMonochromaticBetweenToSetOfDecidableEqOfDecidableRelAdj {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} {C : G.EdgeLabelling K} [DecidableEq V] [DecidableEq K] [DecidableRel G.Adj] {X Y : Finset V} {k : K} : Decidable (C.MonochromaticBetween (↑X) (↑Y) k)

Equations

• SimpleGraph.EdgeLabelling.instDecidableMonochromaticBetweenToSetOfDecidableEqOfDecidableRelAdj = ⋯.mpr Multiset.decidableForallMultiset

@[simp]

theorem SimpleGraph.EdgeLabelling.monochromaticBetween_empty_left {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} {C : G.EdgeLabelling K} {Y : Set V} {k : K} : C.MonochromaticBetween ∅ Y k

@[simp]

theorem SimpleGraph.EdgeLabelling.monochromaticBetween_empty_right {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} {C : G.EdgeLabelling K} {X : Set V} {k : K} : C.MonochromaticBetween X ∅ k

theorem SimpleGraph.EdgeLabelling.monochromaticBetween_singleton_left {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} {C : G.EdgeLabelling K} {x : V} {Y : Set V} {k : K} : C.MonochromaticBetween {x} Y k ↔ ∀ ⦃y : V⦄, y ∈ Y → ∀ (h : G.Adj x y), C.get x y h = k

theorem SimpleGraph.EdgeLabelling.monochromaticBetween_singleton_right {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} {C : G.EdgeLabelling K} {y : V} {X : Set V} {k : K} : C.MonochromaticBetween X {y} k ↔ ∀ ⦃x : V⦄, x ∈ X → ∀ (h : G.Adj x y), C.get x y h = k

theorem SimpleGraph.EdgeLabelling.monochromaticBetween_union_left {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} {C : G.EdgeLabelling K} [DecidableEq V] {X Y Z : Set V} {k : K} : C.MonochromaticBetween (X ∪ Y) Z k ↔ C.MonochromaticBetween X Z k ∧ C.MonochromaticBetween Y Z k

theorem SimpleGraph.EdgeLabelling.monochromaticBetween_union_right {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} {C : G.EdgeLabelling K} [DecidableEq V] {X Y Z : Set V} {k : K} : C.MonochromaticBetween X (Y ∪ Z) k ↔ C.MonochromaticBetween X Y k ∧ C.MonochromaticBetween X Z k

theorem SimpleGraph.EdgeLabelling.monochromaticBetween_self {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} {C : G.EdgeLabelling K} {X : Set V} {k : K} : C.MonochromaticBetween X X k ↔ C.MonochromaticOf X k

theorem SimpleGraph.EdgeLabelling.MonochromaticBetween.subset_left {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} {C : G.EdgeLabelling K} {X Y Z : Set V} {k : K} (hYZ : C.MonochromaticBetween Y Z k) (hXY : X ⊆ Y) : C.MonochromaticBetween X Z k

theorem SimpleGraph.EdgeLabelling.MonochromaticBetween.subset_right {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} {C : G.EdgeLabelling K} {X Y Z : Set V} {k : K} (hXZ : C.MonochromaticBetween X Z k) (hXY : Y ⊆ Z) : C.MonochromaticBetween X Y k

theorem SimpleGraph.EdgeLabelling.MonochromaticBetween.subset {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} {C : G.EdgeLabelling K} {W X Y Z : Set V} {k : K} (hWX : C.MonochromaticBetween W X k) (hYW : Y ⊆ W) (hZX : Z ⊆ X) : C.MonochromaticBetween Y Z k

theorem SimpleGraph.EdgeLabelling.MonochromaticBetween.image {V : Type u_1} {V' : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph V'} {K : Type u_3} {C : G'.EdgeLabelling K} {X Y : Set V} {k : K} {f : G ↪g G'} (hXY : (C.pullback f).MonochromaticBetween X Y k) : C.MonochromaticBetween (⇑f '' X) (⇑f '' Y) k

theorem SimpleGraph.EdgeLabelling.MonochromaticBetween.symm {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} {C : G.EdgeLabelling K} {X Y : Set V} {k : K} (hXY : C.MonochromaticBetween X Y k) : C.MonochromaticBetween Y X k

theorem SimpleGraph.EdgeLabelling.MonochromaticBetween.comm {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} {C : G.EdgeLabelling K} {X Y : Set V} {k : K} : C.MonochromaticBetween Y X k ↔ C.MonochromaticBetween X Y k

theorem SimpleGraph.EdgeLabelling.monochromaticOf_union {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} {C : G.EdgeLabelling K} {X Y : Set V} {k : K} : C.MonochromaticOf (X ∪ Y) k ↔ C.MonochromaticOf X k ∧ C.MonochromaticOf Y k ∧ C.MonochromaticBetween X Y k

theorem SimpleGraph.EdgeLabelling.monochromaticOf_insert {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} {m : Set V} {c : K} {C : G.EdgeLabelling K} [DecidableEq V] {y : V} : C.MonochromaticOf (insert y m) c ↔ C.MonochromaticOf m c ∧ C.MonochromaticBetween m {y} c

theorem SimpleGraph.TopEdgeLabelling.monochromaticOf_insert {V : Type u_1} {K : Type u_3} [DecidableEq V] {C : TopEdgeLabelling V K} {c : K} {m : Set V} {x : V} (hx : x ∉ m) : EdgeLabelling.MonochromaticOf C (insert x m) c ↔ EdgeLabelling.MonochromaticOf C m c ∧ ∀ ⦃y : V⦄ (H : y ∈ m), EdgeLabelling.get C x y ⋯ = c

theorem SimpleGraph.TopEdgeLabelling.Disjoint.monochromaticBetween {V : Type u_1} {K : Type u_3} {C : TopEdgeLabelling V K} {X Y : Set V} {k : K} (h : Disjoint X Y) : EdgeLabelling.MonochromaticBetween C X Y k ↔ ∀ ⦃x : V⦄ (hx : x ∈ X) ⦃y : V⦄ (hy : y ∈ Y), EdgeLabelling.get C x y ⋯ = k

def SimpleGraph.IsRamseyValid {K : Type u_3} (V : Type u_5) (n : K → ℕ) : Prop

The predicate is_ramsey_valid V n says that the type V is large enough to guarantee a clique of size n k for some colour k : K.

Equations

• SimpleGraph.IsRamseyValid V n = ∀ (C : SimpleGraph.TopEdgeLabelling V K), ∃ (m : Finset V) (c : K), SimpleGraph.EdgeLabelling.MonochromaticOf C (↑m) c ∧ n c ≤ m.card

theorem SimpleGraph.IsRamseyValid.empty_colours {K : Type u_3} [IsEmpty K] {n : K → ℕ} : IsRamseyValid (Fin 2) n

theorem SimpleGraph.IsRamseyValid.exists_zero_of_isEmpty {V : Type u_1} {K : Type u_3} [IsEmpty V] {n : K → ℕ} (h : IsRamseyValid V n) : ∃ (c : K), n c = 0

theorem SimpleGraph.isRamseyValid_of_zero {V : Type u_1} {K : Type u_3} {n : K → ℕ} (c : K) (hc : n c = 0) : IsRamseyValid V n

theorem SimpleGraph.isRamseyValid_of_exists_zero {V : Type u_1} {K : Type u_3} (n : K → ℕ) (h : ∃ (c : K), n c = 0) : IsRamseyValid V n

theorem SimpleGraph.IsRamseyValid.mono_right {V : Type u_1} {K : Type u_3} {n n' : K → ℕ} (h : n ≤ n') (h' : IsRamseyValid V n') : IsRamseyValid V n

theorem SimpleGraph.isRamseyValid_iff_eq {V : Type u_1} {K : Type u_3} {n : K → ℕ} : IsRamseyValid V n ↔ ∀ (C : TopEdgeLabelling V K), ∃ (m : Finset V) (c : K), EdgeLabelling.MonochromaticOf C (↑m) c ∧ n c = m.card

theorem SimpleGraph.isRamseyValid_iff_embedding_aux {V : Type u_1} {K : Type u_3} {C : TopEdgeLabelling V K} {n : ℕ} (c : K) : (∃ (m : Finset V), EdgeLabelling.MonochromaticOf C (↑m) c ∧ n = m.card) ↔ Nonempty (⊤ ↪g EdgeLabelling.labelGraph C c)

theorem SimpleGraph.isRamseyValid_iff_embedding {V : Type u_1} {K : Type u_3} {n : K → ℕ} : IsRamseyValid V n ↔ ∀ (C : TopEdgeLabelling V K), ∃ (c : K), Nonempty (⊤ ↪g EdgeLabelling.labelGraph C c)

theorem SimpleGraph.IsRamseyValid.embedding {V : Type u_1} {V' : Type u_2} {K : Type u_3} {n : K → ℕ} (f : V ↪ V') (h' : IsRamseyValid V n) : IsRamseyValid V' n

theorem SimpleGraph.IsRamseyValid.card_fin {V : Type u_1} {K : Type u_3} [Fintype V] {N : ℕ} {n : K → ℕ} (h : N ≤ Fintype.card V) (h' : IsRamseyValid (Fin N) n) : IsRamseyValid V n

theorem SimpleGraph.IsRamseyValid.equiv_left {V : Type u_1} {V' : Type u_2} {K : Type u_3} (n : K → ℕ) (f : V ≃ V') : IsRamseyValid V n ↔ IsRamseyValid V' n

theorem SimpleGraph.IsRamseyValid.equiv_right {V : Type u_1} {K : Type u_3} {K' : Type u_4} {n : K → ℕ} (f : K' ≃ K) (h : IsRamseyValid V n) : IsRamseyValid V (n ∘ ⇑f)

theorem SimpleGraph.isRamseyValid_equiv_right {V : Type u_1} {K : Type u_3} {K' : Type u_4} {n : K → ℕ} (f : K' ≃ K) : IsRamseyValid V (n ∘ ⇑f) ↔ IsRamseyValid V n

instance SimpleGraph.instDecidableIsRamseyValidOfDecidableEqOfFintype {V : Type u_1} {K : Type u_3} [DecidableEq K] [Fintype K] [DecidableEq V] [Fintype V] (n : K → ℕ) : Decidable (IsRamseyValid V n)

Equations

• SimpleGraph.instDecidableIsRamseyValidOfDecidableEqOfFintype n = Fintype.decidableForallFintype

theorem SimpleGraph.ramsey_base {V : Type u_1} {K : Type u_3} [Nonempty V] {n : K → ℕ} (hn : ∃ (k : K), n k ≤ 1) : IsRamseyValid V n

theorem SimpleGraph.ramsey_base' {V : Type u_1} {K : Type u_3} [Fintype V] (n : K → ℕ) (hn : ∃ (k : K), n k ≤ 1) (hV : 1 ≤ Fintype.card V) : IsRamseyValid V n

theorem SimpleGraph.isRamseyValid_min {V : Type u_1} {K : Type u_3} [Fintype V] [Nonempty K] {n : K → ℕ} {n' : ℕ} (h : IsRamseyValid V n) (hn : ∀ (k : K), n' ≤ n k) : n' ≤ Fintype.card V

theorem SimpleGraph.isRamseyValid_unique {V : Type u_1} {K : Type u_3} [Fintype V] [Unique K] {n : K → ℕ} (hV : n default ≤ Fintype.card V) : IsRamseyValid V n

theorem SimpleGraph.IsRamseyValid.remove_twos {V : Type u_1} {K : Type u_3} {n : K → ℕ} (h : IsRamseyValid V n) : IsRamseyValid V fun (k : { k : K // n k ≠ 2 }) => n ↑k

theorem SimpleGraph.IsRamseyValid.of_remove_twos {V : Type u_1} {K : Type u_3} {n : K → ℕ} (h : IsRamseyValid V fun (k : { k : K // n k ≠ 2 }) => n ↑k) : IsRamseyValid V n

theorem SimpleGraph.isRamseyValid_iff_remove_twos {V : Type u_1} {K : Type u_3} (n : K → ℕ) : (IsRamseyValid V fun (k : { k : K // n k ≠ 2 }) => n ↑k) ↔ IsRamseyValid V n

theorem SimpleGraph.isRamseyValid_two {V : Type u_1} {K : Type u_3} {K' : Type u_4} {n : K → ℕ} {n' : K' → ℕ} (f : K' → K) (hf : ∀ (x : K'), n' x ≠ 2 → n (f x) ≠ 2) (hf_inj : ∀ (x y : K'), n' x ≠ 2 → n' y ≠ 2 → f x = f y → x = y) (hf_surj : ∀ (x : K), n x ≠ 2 → ∃ (y : K'), n' y ≠ 2 ∧ f y = x) (hf_comm : ∀ (x : K'), n' x ≠ 2 → n (f x) = n' x) : IsRamseyValid V n' ↔ IsRamseyValid V n

theorem SimpleGraph.ramsey_fin_induct_aux {K : Type u_3} {V : Type u_5} [DecidableEq K] {n : K → ℕ} (N : K → ℕ) {C : TopEdgeLabelling V K} (m : K → Finset V) (x : V) (hN : ∀ (k : K), IsRamseyValid (Fin (N k)) (Function.update n k (n k - 1))) (hx : ∀ (k : K), x ∉ m k) (h : ∃ (k : K), N k ≤ (m k).card) (hm : ∀ (k : K) (y : V) (hy : y ∈ m k), EdgeLabelling.get C x y ⋯ = k) : ∃ (m : Finset V) (c : K), EdgeLabelling.MonochromaticOf C (↑m) c ∧ n c ≤ m.card

theorem SimpleGraph.ramsey_fin_induct {K : Type u_3} [DecidableEq K] [Fintype K] (n N : K → ℕ) (hN : ∀ (k : K), IsRamseyValid (Fin (N k)) (Function.update n k (n k - 1))) : IsRamseyValid (Fin (∑ k : K, (N k - 1) + 2)) n

theorem SimpleGraph.ramsey_fin_exists {K : Type u_3} [Finite K] (n : K → ℕ) : ∃ (N : ℕ), IsRamseyValid (Fin N) n

theorem SimpleGraph.ramsey_fin_induct' {K : Type u_3} [DecidableEq K] [Fintype K] (n N : K → ℕ) (hn : ∀ (k : K), 2 ≤ n k) (hN : ∀ (k : K), IsRamseyValid (Fin (N k)) (Function.update n k (n k - 1))) : IsRamseyValid (Fin (∑ k : K, N k + 2 - Fintype.card K)) n

theorem SimpleGraph.ramsey_fin_induct_two {i j Ni Nj : ℕ} (hi : 2 ≤ i) (hj : 2 ≤ j) (hi' : IsRamseyValid (Fin Ni) ![i - 1, j]) (hj' : IsRamseyValid (Fin Nj) ![i, j - 1]) : IsRamseyValid (Fin (Ni + Nj)) ![i, j]

theorem SimpleGraph.ramsey_fin_induct_two_evens {i j Ni Nj : ℕ} (hi : 2 ≤ i) (hj : 2 ≤ j) (hNi : Even Ni) (hNj : Even Nj) (hi' : IsRamseyValid (Fin Ni) ![i - 1, j]) (hj' : IsRamseyValid (Fin Nj) ![i, j - 1]) : IsRamseyValid (Fin (Ni + Nj - 1)) ![i, j]

theorem SimpleGraph.ramsey_fin_induct_three {i j k Ni Nj Nk : ℕ} (hi : 2 ≤ i) (hj : 2 ≤ j) (hk : 2 ≤ k) (hi' : IsRamseyValid (Fin Ni) ![i - 1, j, k]) (hj' : IsRamseyValid (Fin Nj) ![i, j - 1, k]) (hk' : IsRamseyValid (Fin Nk) ![i, j, k - 1]) : IsRamseyValid (Fin (Ni + Nj + Nk - 1)) ![i, j, k]

def SimpleGraph.ramseyNumber {K : Type u_3} [DecidableEq K] [Fintype K] (n : K → ℕ) : ℕ

Given a tuple n : K → ℕ of naturals indexed by K, define the ramsey number as the smallest N such that any labelling of the complete graph on N vertices with K labels contains a subset of size n k in which every edge is labelled k. While this definition is computable, it is not at all efficient to compute.

Equations

• SimpleGraph.ramseyNumber n = Nat.find ⋯

theorem SimpleGraph.ramseyNumber_spec_fin {K : Type u_3} [DecidableEq K] [Fintype K] (n : K → ℕ) : IsRamseyValid (Fin (ramseyNumber n)) n

theorem SimpleGraph.ramseyNumber_spec {V : Type u_1} {K : Type u_3} {n : K → ℕ} [Fintype V] [DecidableEq K] [Fintype K] (h : ramseyNumber n ≤ Fintype.card V) : IsRamseyValid V n

theorem SimpleGraph.ramseyNumber_min_fin {K : Type u_3} {n : K → ℕ} {N : ℕ} [DecidableEq K] [Fintype K] (hN : IsRamseyValid (Fin N) n) : ramseyNumber n ≤ N

theorem SimpleGraph.ramseyNumber_min {V : Type u_1} {K : Type u_3} {n : K → ℕ} [Fintype V] [DecidableEq K] [Fintype K] (hN : IsRamseyValid V n) : ramseyNumber n ≤ Fintype.card V

theorem SimpleGraph.ramseyNumber_le_iff {V : Type u_1} {K : Type u_3} {n : K → ℕ} [Fintype V] [DecidableEq K] [Fintype K] : ramseyNumber n ≤ Fintype.card V ↔ IsRamseyValid V n

theorem SimpleGraph.ramseyNumber_le_iff_fin {K : Type u_3} {n : K → ℕ} {N : ℕ} [DecidableEq K] [Fintype K] : ramseyNumber n ≤ N ↔ IsRamseyValid (Fin N) n

theorem SimpleGraph.ramseyNumber_eq_of {K : Type u_3} {n : K → ℕ} {N : ℕ} [DecidableEq K] [Fintype K] (h : IsRamseyValid (Fin (N + 1)) n) (h' : ¬IsRamseyValid (Fin N) n) : ramseyNumber n = N + 1

theorem SimpleGraph.ramseyNumber_congr {K : Type u_3} {K' : Type u_4} [DecidableEq K'] [Fintype K'] {n : K → ℕ} [DecidableEq K] [Fintype K] {n' : K' → ℕ} (h : ∀ (N : ℕ), IsRamseyValid (Fin N) n ↔ IsRamseyValid (Fin N) n') : ramseyNumber n = ramseyNumber n'

theorem SimpleGraph.ramseyNumber_equiv {K : Type u_3} {K' : Type u_4} [DecidableEq K'] [Fintype K'] {n : K → ℕ} [DecidableEq K] [Fintype K] (f : K' ≃ K) : ramseyNumber (n ∘ ⇑f) = ramseyNumber n

theorem SimpleGraph.ramseyNumber_first_swap {i : ℕ} (x y : ℕ) (t : Fin i → ℕ) : ramseyNumber (Matrix.vecCons x (Matrix.vecCons y t)) = ramseyNumber (Matrix.vecCons y (Matrix.vecCons x t))

theorem SimpleGraph.ramseyNumber_pair_swap (x y : ℕ) : ramseyNumber ![x, y] = ramseyNumber ![y, x]

theorem SimpleGraph.ramseyNumber.eq_zero_iff {K : Type u_3} {n : K → ℕ} [DecidableEq K] [Fintype K] : ramseyNumber n = 0 ↔ ∃ (c : K), n c = 0

theorem SimpleGraph.ramseyNumber.exists_zero_of_eq_zero {K : Type u_3} {n : K → ℕ} [DecidableEq K] [Fintype K] (h : ramseyNumber n = 0) : ∃ (c : K), n c = 0

theorem SimpleGraph.ramseyNumber_exists_zero {K : Type u_3} {n : K → ℕ} [DecidableEq K] [Fintype K] (c : K) (hc : n c = 0) : ramseyNumber n = 0

theorem SimpleGraph.ramseyNumber_pos {K : Type u_3} {n : K → ℕ} [DecidableEq K] [Fintype K] : 0 < ramseyNumber n ↔ ∀ (c : K), n c ≠ 0

theorem SimpleGraph.ramseyNumber_le_one {K : Type u_3} {n : K → ℕ} [DecidableEq K] [Fintype K] (hc : ∃ (c : K), n c ≤ 1) : ramseyNumber n ≤ 1

theorem SimpleGraph.ramseyNumber_ge_min {K : Type u_3} {n : K → ℕ} [DecidableEq K] [Fintype K] [Nonempty K] (i : ℕ) (hk : ∀ (k : K), i ≤ n k) : i ≤ ramseyNumber n

theorem SimpleGraph.exists_le_of_ramseyNumber_le {K : Type u_3} {n : K → ℕ} [DecidableEq K] [Fintype K] [Nonempty K] (i : ℕ) (hi : ramseyNumber n ≤ i) : ∃ (k : K), n k ≤ i

@[simp]

theorem SimpleGraph.ramseyNumber_empty {K : Type u_3} {n : K → ℕ} [DecidableEq K] [Fintype K] [IsEmpty K] : ramseyNumber n = 2

theorem SimpleGraph.ramseyNumber_nil : ramseyNumber ![] = 2

theorem SimpleGraph.exists_le_one_of_ramseyNumber_le_one {K : Type u_3} {n : K → ℕ} [DecidableEq K] [Fintype K] (hi : ramseyNumber n ≤ 1) : ∃ (k : K), n k ≤ 1

theorem SimpleGraph.ramseyNumber_eq_one {K : Type u_3} {n : K → ℕ} [DecidableEq K] [Fintype K] (hc : ∃ (c : K), n c = 1) (hc' : ∀ (c : K), n c ≠ 0) : ramseyNumber n = 1

theorem SimpleGraph.ramseyNumber_eq_one_iff {K : Type u_3} {n : K → ℕ} [DecidableEq K] [Fintype K] : ((∃ (c : K), n c = 1) ∧ ∀ (c : K), n c ≠ 0) ↔ ramseyNumber n = 1

theorem SimpleGraph.ramseyNumber_unique_colour {K : Type u_3} {n : K → ℕ} [DecidableEq K] [Fintype K] [Unique K] : ramseyNumber n = n default

@[simp]

theorem SimpleGraph.ramseyNumber_singleton {i : ℕ} : ramseyNumber ![i] = i

theorem SimpleGraph.ramseyNumber.mono {K : Type u_3} [DecidableEq K] [Fintype K] {n n' : K → ℕ} (h : n ≤ n') : ramseyNumber n ≤ ramseyNumber n'

theorem SimpleGraph.ramseyNumber.mono_two {a b c d : ℕ} (hab : a ≤ b) (hcd : c ≤ d) : ramseyNumber ![a, c] ≤ ramseyNumber ![b, d]

theorem SimpleGraph.ramseyNumber_monotone {i : ℕ} : Monotone ramseyNumber

theorem SimpleGraph.ramseyNumber_remove_two {K : Type u_3} {K' : Type u_4} [DecidableEq K'] [Fintype K'] [DecidableEq K] [Fintype K] {n : K → ℕ} {n' : K' → ℕ} (f : K' → K) (hf : ∀ (x : K'), n' x ≠ 2 → n (f x) ≠ 2) (hf_inj : ∀ (x y : K'), n' x ≠ 2 → n' y ≠ 2 → f x = f y → x = y) (hf_surj : ∀ (x : K), n x ≠ 2 → ∃ (y : K'), n' y ≠ 2 ∧ f y = x) (hf_comm : ∀ (x : K'), n' x ≠ 2 → n (f x) = n' x) : ramseyNumber n' = ramseyNumber n

@[simp]

theorem SimpleGraph.ramseyNumber_cons_two {i : ℕ} {n : Fin i → ℕ} : ramseyNumber (Matrix.vecCons 2 n) = ramseyNumber n

@[simp]

theorem SimpleGraph.ramseyNumber_cons_zero {i : ℕ} {n : Fin i → ℕ} : ramseyNumber (Matrix.vecCons 0 n) = 0

theorem SimpleGraph.ramseyNumber_cons_one_of_one_le {i : ℕ} {n : Fin i → ℕ} (h : ∀ (k : Fin i), n k ≠ 0) : ramseyNumber (Matrix.vecCons 1 n) = 1

theorem SimpleGraph.ramseyNumber_one_succ {i : ℕ} : ramseyNumber ![1, i + 1] = 1

theorem SimpleGraph.ramseyNumber_succ_one {i : ℕ} : ramseyNumber ![i + 1, 1] = 1

theorem SimpleGraph.ramseyNumber_two_left {i : ℕ} : ramseyNumber ![2, i] = i

@[simp]

theorem SimpleGraph.ramseyNumber_two_right {i : ℕ} : ramseyNumber ![i, 2] = i

theorem SimpleGraph.ramseyNumber_multicolour_bound {K : Type u_3} {n : K → ℕ} [DecidableEq K] [Fintype K] (h : ∀ (k : K), 2 ≤ n k) : ramseyNumber n ≤ ∑ k : K, ramseyNumber (Function.update n k (n k - 1)) + 2 - Fintype.card K

theorem SimpleGraph.ramseyNumber_two_colour_bound_aux {i j : ℕ} (hi : 2 ≤ i) (hj : 2 ≤ j) : ramseyNumber ![i, j] ≤ ramseyNumber ![i - 1, j] + ramseyNumber ![i, j - 1]

theorem SimpleGraph.ramseyNumber_two_colour_bound (i j : ℕ) (hij : i ≠ 1 ∨ j ≠ 1) : ramseyNumber ![i, j] ≤ ramseyNumber ![i - 1, j] + ramseyNumber ![i, j - 1]

theorem SimpleGraph.ramseyNumber_two_colour_bound_even {i j : ℕ} (Ni Nj : ℕ) (hi : 2 ≤ i) (hj : 2 ≤ j) (hNi : ramseyNumber ![i - 1, j] ≤ Ni) (hNj : ramseyNumber ![i, j - 1] ≤ Nj) (hNi' : Even Ni) (hNj' : Even Nj) : ramseyNumber ![i, j] ≤ Ni + Nj - 1

theorem SimpleGraph.ramseyNumber_three_colour_bound {i j k : ℕ} (hi : 2 ≤ i) (hj : 2 ≤ j) (hk : 2 ≤ k) : ramseyNumber ![i, j, k] ≤ ramseyNumber ![i - 1, j, k] + ramseyNumber ![i, j - 1, k] + ramseyNumber ![i, j, k - 1] - 1

def SimpleGraph.diagonalRamsey (k : ℕ) : ℕ

The diagonal ramsey number, defined by R(k, k).

Equations

• SimpleGraph.diagonalRamsey k = SimpleGraph.ramseyNumber ![k, k]

theorem SimpleGraph.diagonalRamsey.def {k : ℕ} : diagonalRamsey k = ramseyNumber ![k, k]

@[simp]

theorem SimpleGraph.diagonalRamsey_zero : diagonalRamsey 0 = 0

@[simp]

theorem SimpleGraph.diagonalRamsey_one : diagonalRamsey 1 = 1

@[simp]

theorem SimpleGraph.diagonalRamsey_two : diagonalRamsey 2 = 2

theorem SimpleGraph.diagonalRamsey_monotone : Monotone diagonalRamsey

@[irreducible]

theorem SimpleGraph.ramseyNumber_le_choose (i j : ℕ) : ramseyNumber ![i, j] ≤ (i + j - 2).choose (i - 1)

theorem SimpleGraph.diagonalRamsey_le_centralBinom (i : ℕ) : diagonalRamsey i ≤ (i - 1).centralBinom

theorem SimpleGraph.diagonalRamsey_le_central_binom' (i : ℕ) : diagonalRamsey i ≤ i.centralBinom

theorem SimpleGraph.ramseyNumber_pair_le_two_pow {i j : ℕ} : ramseyNumber ![i, j] ≤ 2 ^ (i + j - 2)

theorem SimpleGraph.ramseyNumber_pair_le_two_pow' {i j : ℕ} : ramseyNumber ![i, j] ≤ 2 ^ (i + j)

theorem SimpleGraph.diagonalRamsey_le_four_pow_sub_one {i : ℕ} : diagonalRamsey i ≤ 4 ^ (i - 1)

theorem SimpleGraph.diagonalRamsey_le_four_pow {i : ℕ} : diagonalRamsey i ≤ 4 ^ i

theorem SimpleGraph.ramseyNumber_le_right_pow_left (i j : ℕ) : ramseyNumber ![i, j] ≤ j ^ (i - 1)

A good bound when i is small and j is large. For i = 1, 2 this is equality (as long as j ≠ 0), and for i = 3 and i = 4 it is the best possible polynomial upper bound, although lower order improvements are available.

theorem SimpleGraph.ramseyNumber_le_right_pow_left' {i j : ℕ} : ramseyNumber ![i, j] ≤ j ^ i

A simplification of ramsey_number_le_right_pow_left which is more convenient for asymptotic reasoning. A good bound when i is small and j is very large.