Documentation

FormalRamsey.Ramsey2Color

def Ramsey₂Prop (N s t : ℕ) :

Equations

Ramsey₂Prop N s t = Ramsey.RamseyProp N (s ::ᵥ t ::ᵥ List.Vector.nil)

Instances For

instance instDecidablePredNatMemSetSetOfRamsey₂Prop {s t : ℕ} :

DecidablePred (Membership.mem {N : ℕ | Ramsey₂Prop N s t})

Equations

instDecidablePredNatMemSetSetOfRamsey₂Prop = id inferInstance

def Ramsey₂GraphProp (N s t : ℕ) :

Ramsey₂Prop N s t ↔ RamseyGraphProp N s t

Equations

⋯ = ⋯

Instances For

theorem Ramsey₂PropSymm {N s t : ℕ} :

Ramsey₂Prop N s t ↔ Ramsey₂Prop N t s

theorem friendshipUpperbound :

Ramsey₂Prop 6 3 3

theorem Ramsey₂Prop1 (N k : ℕ) :

Ramsey₂Prop N.succ 1 k

theorem Ramsey₂PropIneq {M N s t : ℕ} :

0 < M + N → Ramsey₂Prop M s t.succ → Ramsey₂Prop N s.succ t → Ramsey₂Prop (M + N) s.succ t.succ

theorem Ramsey₂Finite (s t : ℕ) :

{N : ℕ | Ramsey₂Prop N s t}.Nonempty

def Ramsey₂ (s t : ℕ) :

Equations

Ramsey₂ s t = Nat.find ⋯

Instances For

theorem Ramsey₂2 (k : ℕ) :

Ramsey₂ 2 k.succ = k.succ

theorem Ramsey₂1 (k : ℕ) :

Ramsey₂ 1 k.succ = 1

theorem Ramsey₂PropStrictIneq {M N s t : ℕ} :

Odd M → Odd N → Ramsey₂Prop M.succ s t.succ → Ramsey₂Prop N.succ s.succ t → Ramsey₂Prop (M + N).succ s.succ t.succ

theorem Ramsey₂ToRamsey₂Prop {N s t : ℕ} :

Ramsey₂ s t = N → Ramsey₂Prop N s t

theorem Ramsey₂Ineq (s t : ℕ) :

0 < Ramsey₂ s t.succ + Ramsey₂ s.succ t → Ramsey₂ s.succ t.succ ≤ Ramsey₂ s t.succ + Ramsey₂ s.succ t

theorem Ramsey₂0 {s : ℕ} :

Ramsey₂ 0 s = 0

theorem Ramsey₂Symm {s t : ℕ} :

Ramsey₂ s t = Ramsey₂ t s

theorem Ramsey₂StrictIneq (s t : ℕ) :

0 < Ramsey₂ s t.succ + Ramsey₂ s.succ t → Even (Ramsey₂ s t.succ) → Even (Ramsey₂ s.succ t) → Ramsey₂ s.succ t.succ < Ramsey₂ s t.succ + Ramsey₂ s.succ t

theorem friendship_upper_bound_alt :

Ramsey₂ 3 3 ≤ 6

theorem Ramsey₂ByList (N s t : ℕ) :

Ramsey₂Prop N s.succ t.succ ↔ ∀ (f : Sym2 (Fin N) → Fin 2), (∃ l ∈ List.sublistsLen s.succ (List.finRange N), List.Pairwise (fun (u v : Fin N) => f s(u, v) = 0) l) ∨ ∃ l ∈ List.sublistsLen t.succ (List.finRange N), List.Pairwise (fun (u v : Fin N) => f s(u, v) = 1) l

theorem friendship :

Ramsey₂ 3 3 = 6

theorem R43 :

Ramsey₂ 4 3 = 9

theorem R53 :

Ramsey₂ 5 3 = 14

theorem R44 :

Ramsey₂ 4 4 = 18

theorem Ramsey₂_binomial_coefficient_ineq (s t : ℕ) :

Ramsey₂ s.succ t.succ ≤ (s + t).choose s