Documentation

Ramsey2lemmas.Inequalities

@[simp]

theorem Fin.val_three (n : ℕ) :

↑3 = 3

theorem SimpleGraph.σ_helper {N x y k : ℕ} {G : SimpleGraph (Fin N.succ)} [DecidableRel G.Adj] (hxy : G.isXYGraph x.succ y.succ) (σlt : σ_G hxy < k) (f : ℕ → ℕ) :

(∀ i ∈ Finset.range k \ Finset.range (σ_G hxy).succ, f i = 0) → (Finset.range (σ_G hxy).succ).sum f = (Finset.range k).sum f

theorem SimpleGraph.sᵢ_vanish {N x y : ℕ} {G : SimpleGraph (Fin N.succ)} [DecidableRel G.Adj] (hxy : G.isXYGraph x.succ y.succ) (Ngt : RamseyOld x.succ y < N) (k i : ℕ) :

i ∈ Finset.range k \ Finset.range (σ_G hxy).succ → ∀ (n : ℕ), n * G.sᵢ x y i = 0

axiom SimpleGraph.R36ub :

RamseyOld 3 6 ≤ 17

theorem SimpleGraph.R36 :

RamseyOld 3 6 = 17

axiom SimpleGraph.R37ub :

RamseyOld 3 7 ≤ 22

theorem SimpleGraph.R37 :

RamseyOld 3 7 = 22

axiom SimpleGraph.e3_6_11_11 :

e 3 6 11 ≥ 11

axiom SimpleGraph.e3_6_12_15 :

e 3 6 12 ≥ 15

axiom SimpleGraph.e3_6_13_20 :

e 3 6 13 ≥ 20

axiom SimpleGraph.e3_6_14_25 :

e 3 6 14 ≥ 25

axiom SimpleGraph.e3_6_15_32 :

e 3 6 15 ≥ 32

axiom SimpleGraph.e3_6_16_40 :

e 3 6 16 ≥ 40

theorem SimpleGraph.R38lb :

27 ∈ {N : ℕ | ∃ (G : SimpleGraph (Fin N)), Nonempty (DecidableRel G.Adj) ∧ G.isXYGraph 3 8}

theorem SimpleGraph.e3_7_18_36 :

e 3 7 18 ≥ 36

axiom SimpleGraph.e3_7_19_44 :

e 3 7 19 ≥ 44

theorem SimpleGraph.e3_7_20_50 :

e 3 7 20 ≥ 50

theorem SimpleGraph.e3_7_21_59 :

e 3 7 21 ≥ 59

theorem SimpleGraph.Ineq₉ :

e 3 8 26 ≥ 80

theorem SimpleGraph.Ineq₁₀ (h : RamseyOld 3 8 > 27) :

e 3 8 27 ≥ 88

theorem SimpleGraph.Ineq₁₁ (h : RamseyOld 3 8 > 28) :

e 3 8 28 ≥ 99

theorem SimpleGraph.regular_of_isXY {x y : ℕ} (N : ℕ) (G : SimpleGraph (Fin N.succ)) [DecidableRel G.Adj] :

G.isXYGraph x.succ y.succ → N ≥ RamseyOld x y.succ + RamseyOld x.succ y → G.IsRegularOfDegree (RamseyOld x y.succ)

theorem SimpleGraph.R39Ineq {G : SimpleGraph (Fin 36)} [DecidableRel G.Adj] (hxy : G.isXYGraph 3 9) :

G.edgeFinset.card ≥ 144

theorem SimpleGraph.R39_36_graph_IsRegular8 {G : SimpleGraph (Fin 36)} [DecidableRel G.Adj] (hxy : G.isXYGraph 3 9) :

G.IsRegularOfDegree 8

theorem SimpleGraph.R39_36_graph_has_R38_27 {G : SimpleGraph (Fin 36)} [DecidableRel G.Adj] (hxy : G.isXYGraph 3 9) :

∃ (s : Finset (Fin 36)), s.card = 27 ∧ (induce (↑s) G).isXYGraph 3 8