Documentation

Ramsey2lemmas.Theory

theorem Int.isAddUnit (z : ℤ) :

def SimpleGraph.isXYGraph {V : Type u_1} (G : SimpleGraph V) (x y : ℕ) :

Equations

G.isXYGraph x y = (G.cliqueNum < x ∧ G.indepNum < y)

Instances For

noncomputable def SimpleGraph.RamseyOld (x y : ℕ) :

Equations

SimpleGraph.RamseyOld x y = sSup {N : ℕ | ∃ (G : SimpleGraph (Fin N)) (x_1 : DecidableRel G.Adj), G.isXYGraph x y}

Instances For

theorem SimpleGraph.Lemma₁ {V : Type u_1} (G : SimpleGraph V) (x y : ℕ) :

G.isXYGraph x y ↔ Gᶜ.isXYGraph y x

theorem SimpleGraph.noXYGraphIffRamseyGraphProp (x y N : ℕ) :

(∀ (G : SimpleGraph (Fin N)), ¬G.isXYGraph x y) ↔ RamseyGraphProp N x y

theorem SimpleGraph.isXYGraph_bddAbove (x y : ℕ) :

BddAbove {N : ℕ | ∃ (G : SimpleGraph (Fin N)), G.isXYGraph x y}

theorem SimpleGraph.cardLERamseyOld {V : Type u_1} (G : SimpleGraph V) (x y : ℕ) [Fintype V] :

G.isXYGraph x y → Fintype.card V ≤ RamseyOld x y

theorem SimpleGraph.R3y_neighbor_Ind {V : Type u_1} (G : SimpleGraph V) [Fintype V] [DecidableEq V] [DecidableRel G.Adj] {y : ℕ} (hxy : G.isXYGraph 3 y.succ) (p : V) :

G.IsNIndepSet (G.degree p) (G.neighborFinset p)

theorem SimpleGraph.GraphRamsey2RamseyOld (x y : ℕ) :

GraphRamsey x.succ y.succ = RamseyOld x.succ y.succ + 1

theorem SimpleGraph.RamseyOld₂ (y : ℕ) :

RamseyOld 2 y.succ = y

@[reducible, inline]

noncomputable abbrev SimpleGraph.vᵢ (x y i : ℕ) :

Equations

SimpleGraph.vᵢ x y i = SimpleGraph.RamseyOld x y.succ - i

Instances For

@[reducible, inline]

noncomputable abbrev SimpleGraph.sᵢ {V : Type u_1} (G : SimpleGraph V) (x y : ℕ) [Fintype V] (i : ℕ) [DecidableRel G.Adj] :

Equations

G.sᵢ x y i = {v : V | G.degree v = SimpleGraph.vᵢ x y i}.card

Instances For

@[reducible, inline]

noncomputable abbrev SimpleGraph.tᵢ {V : Type u_1} (G : SimpleGraph V) (x y : ℕ) [Fintype V] (i : ℕ) [DecidableRel G.Adj] (p : V) :

Equations

G.tᵢ x y i p = {v ∈ G.neighborFinset p | G.degree v = SimpleGraph.vᵢ x y i}.card

Instances For

noncomputable def SimpleGraph.σ_G {V : Type u_1} {G : SimpleGraph V} {x y : ℕ} [Fintype V] [DecidableRel G.Adj] :

G.isXYGraph x.succ y.succ → ℕ

Equations

SimpleGraph.σ_G x✝ = SimpleGraph.RamseyOld x y.succ - G.minDegree

Instances For

theorem SimpleGraph.sum_degree_eq_sum_over_degrees {V : Type u_1} {G : SimpleGraph V} [Fintype V] [DecidableRel G.Adj] :

∑ v : V, G.degree v = ∑ d ∈ Finset.image (fun (v : V) => G.degree v) Finset.univ, d * {v : V | G.degree v = d}.card

theorem SimpleGraph.num_of_vertices_eq_sum_over_degrees {V : Type u_1} {G : SimpleGraph V} [Fintype V] [DecidableRel G.Adj] :

Fintype.card V = ∑ d ∈ Finset.image (fun (v : V) => G.degree v) Finset.univ, {v : V | G.degree v = d}.card

def SimpleGraph.H₁ {α : Type u_2} (G : SimpleGraph α) (p : α) :

SimpleGraph ↑(G.neighborSet p)

Equations

G.H₁ p = SimpleGraph.induce (G.neighborSet p) G

Instances For

instance SimpleGraph.instDecidableRelElemNeighborSetAdjH₁ {α : Type u_2} (G : SimpleGraph α) [DecidableRel G.Adj] (p : α) :

DecidableRel (G.H₁ p).Adj

Equations

G.instDecidableRelElemNeighborSetAdjH₁ p = SimpleGraph.instDecidableComapAdj (⇑(Function.Embedding.subtype fun (x : α) => x ∈ G.neighborSet p)) G

def SimpleGraph.H₂ {α : Type u_2} (G : SimpleGraph α) (p : α) :

SimpleGraph ↑(Gᶜ.neighborSet p)

Equations

G.H₂ p = SimpleGraph.induce (Gᶜ.neighborSet p) G

Instances For

instance SimpleGraph.instDecidableRelElemNeighborSetComplAdjH₂ {α : Type u_2} (G : SimpleGraph α) [DecidableRel G.Adj] (p : α) :

DecidableRel (G.H₂ p).Adj

Equations

G.instDecidableRelElemNeighborSetComplAdjH₂ p = SimpleGraph.instDecidableComapAdj (⇑(Function.Embedding.subtype fun (x : α) => x ∈ Gᶜ.neighborSet p)) G

@[reducible, inline]

abbrev SimpleGraph.e₁ {α : Type u_2} [Fintype α] (G : SimpleGraph α) [DecidableRel G.Adj] (p : α) :

Equations

G.e₁ p = (G.H₁ p).edgeFinset.card

Instances For

@[reducible, inline]

abbrev SimpleGraph.e₂ {α : Type u_2} [Fintype α] [DecidableEq α] (G : SimpleGraph α) [DecidableRel G.Adj] (p : α) :

Equations

G.e₂ p = (G.H₂ p).edgeFinset.card

Instances For

def SimpleGraph.H₁₂_iso {α : Type u_2} (G : SimpleGraph α) (p : α) :

(G.H₁ p)ᶜ ≃g Gᶜ.H₂ p

Equations

G.H₁₂_iso p = { toFun := fun (v : ↑(G.neighborSet p)) => ⟨↑v, ⋯⟩, invFun := fun (v : ↑(Gᶜ ᶜ.neighborSet p)) => ⟨↑v, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }

Instances For

theorem SimpleGraph.H₁_eq_bot_of_3y {α : Type u_2} {y : ℕ} [Fintype α] [DecidableEq α] (G : SimpleGraph α) [DecidableRel G.Adj] (hxy : G.isXYGraph 3 y.succ) (p : α) :

theorem SimpleGraph.H₁_cliqueNum_lt {N : ℕ} (G : SimpleGraph (Fin N.succ)) (p : Fin N.succ) [DecidableRel G.Adj] :

(G.H₁ p).cliqueNum ≤ G.cliqueNum - 1

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

G.isXYGraph x.succ y.succ → G.degree p ≤ RamseyOld x y.succ ∧ G.degree p + RamseyOld x.succ y ≥ N

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

∑ v : Fin N.succ, G.degree v = ∑ j ∈ Finset.range (σ_G hxy).succ, G.sᵢ x y j * vᵢ x y j

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

N.succ = ∑ i ∈ Finset.range (σ_G hxy + 1), G.sᵢ x y i

theorem SimpleGraph.H₁_degreeCount_eq {x y N : ℕ} (G : SimpleGraph (Fin N.succ)) (p : Fin N.succ) [DecidableRel G.Adj] (hxy : G.isXYGraph x.succ y.succ) :

∑ v ∈ G.neighborFinset p, G.degree v = ∑ j ∈ Finset.range (σ_G hxy).succ, G.tᵢ x y j p * vᵢ x y j

theorem SimpleGraph.H₁_vertCount_eq {x y N : ℕ} (G : SimpleGraph (Fin N.succ)) (p : Fin N.succ) [DecidableRel G.Adj] (hxy : G.isXYGraph x.succ y.succ) :

Fintype.card ↑(G.neighborSet p) = ∑ i ∈ Finset.range (σ_G hxy + 1), G.tᵢ x y i p

theorem SimpleGraph.Prop₁ {x y N : ℕ} {G : SimpleGraph (Fin N.succ)} [DecidableRel G.Adj] (hxy : G.isXYGraph x.succ y.succ) :

N.succ ≤ RamseyOld x y.succ + RamseyOld x.succ y + 1 - σ_G hxy ∧ σ_G hxy ≤ RamseyOld x y.succ + RamseyOld x.succ y + 1 - N.succ

theorem SimpleGraph.vᵢ_deg_swap {x y N : ℕ} {G : SimpleGraph (Fin N.succ)} [DecidableRel G.Adj] (hxy : G.isXYGraph x.succ y.succ) (j : Fin N.succ) (d : Fin (σ_G hxy).succ) :

vᵢ x y (G.degree j) = ↑d ↔ G.degree j = vᵢ x y ↑d

theorem SimpleGraph.Prop₂ (i : ℕ) {x y N : ℕ} {G : SimpleGraph (Fin N.succ)} (p : Fin N.succ) [DecidableRel G.Adj] (hxy : G.isXYGraph x.succ y.succ) (iub : i ≤ RamseyOld x y.succ) (hp : G.degree p = vᵢ x y i) :

2 * (↑(G.e₂ p) - ↑(G.e₁ p)) = ↑(RamseyOld x y.succ) * (↑N.succ - 2 * ↑(RamseyOld x y.succ) + 2 * ↑i) + ∑ j ∈ Finset.range (σ_G hxy).succ, ↑j * (2 * ↑(G.tᵢ x y j p) - ↑(G.sᵢ x y j))

noncomputable def SimpleGraph.e (x y N : ℕ) :

Equations

SimpleGraph.e x y N = sInf {n : ℕ | ∃ (G : SimpleGraph (Fin N.succ)) (x_1 : DecidableRel G.Adj), G.isXYGraph x y ∧ G.edgeFinset.card = n}

Instances For

theorem SimpleGraph.exy0 (x y : ℕ) :

e x y 0 = 0

theorem SimpleGraph.e₂_ge_e {x y N : ℕ} {G : SimpleGraph (Fin N.succ)} (p : Fin N.succ) [DecidableRel G.Adj] (hxy : G.isXYGraph x.succ y.succ) :

G.e₂ p ≥ e x.succ y (N - G.degree p).pred

theorem SimpleGraph.Prop₄ {y N : ℕ} {G : SimpleGraph (Fin N.succ)} [DecidableRel G.Adj] (hxy : G.isXYGraph 3 y.succ) :

N.succ * G.edgeFinset.card ≥ ∑ i ∈ Finset.range (σ_G hxy).succ, (e 3 y (N - vᵢ 2 y i - 1) + vᵢ 2 y i ^ 2) * G.sᵢ 2 y i