Ported to Lean Pool from jtraverso/hajnal-szemeredi, commit ba34061e3cf12dfc8297610d5d7b3f0afac7ec54; import paths adapted.

Definiciones para la prueba de Kierstead–Kostochka del teorema de Hajnal–Szemerédi

Trabajamos con un grafo G sobre un tipo ambiente V y un conjunto finito de vértices S : Finset V (el grafo considerado es el inducido G[S]). Una coloración es una función c : V → ℕ; sólo importan sus valores sobre S, y la paleta es un Finset ℕ.

Esto permite pasar a subgrafos inducidos (A ∪ {y₁}, B \ {y₁} en el artículo) y cambiar la paleta sin cambiar de tipo.

Referencia: H. A. Kierstead, A. V. Kostochka, A short proof of the Hajnal–Szemerédi theorem on equitable colouring, Combin. Probab. Comput. 17 (2008) 265–270.

def HajnalSzemeredi.cls {V : Type u_1} (S : Finset V) (c : V → ℕ) (i : ℕ) : Finset V

La clase de color i de c dentro de S.

Equations

• HajnalSzemeredi.cls S c i = {v ∈ S | c v = i}

noncomputable def HajnalSzemeredi.nbr {V : Type u_1} (G : SimpleGraph V) (S : Finset V) (v : V) : Finset V

Vecinos de v dentro de S.

Equations

• HajnalSzemeredi.nbr G S v = {w ∈ S | G.Adj v w}

def HajnalSzemeredi.Proper {V : Type u_1} (G : SimpleGraph V) (S : Finset V) (c : V → ℕ) : Prop

c es propia sobre S.

Equations

• HajnalSzemeredi.Proper G S c = ∀ v ∈ S, ∀ w ∈ S, G.Adj v w → c v ≠ c w

def HajnalSzemeredi.Into {V : Type u_1} (S : Finset V) (c : V → ℕ) (P : Finset ℕ) : Prop

c toma valores en la paleta P sobre S.

Equations

• HajnalSzemeredi.Into S c P = ∀ v ∈ S, c v ∈ P

def HajnalSzemeredi.DegLe {V : Type u_1} (G : SimpleGraph V) (S : Finset V) (r : ℕ) : Prop

Grado máximo de G[S] a lo más r.

Equations

• HajnalSzemeredi.DegLe G S r = ∀ v ∈ S, (HajnalSzemeredi.nbr G S v).card ≤ r

noncomputable def HajnalSzemeredi.edgeCount {V : Type u_1} (G : SimpleGraph V) (S : Finset V) : ℕ

Número de pares ordenados adyacentes en S (el doble del número de aristas de G[S]).

Equations

• HajnalSzemeredi.edgeCount G S = {p ∈ S.offDiag | G.Adj p.1 p.2}.card

structure HajnalSzemeredi.IsEq {V : Type u_1} (G : SimpleGraph V) (S : Finset V) (P : Finset ℕ) (c : V → ℕ) (s : ℕ) : Prop

Coloración equitativa de S con paleta P, todas las clases de tamaño exactamente s.

• proper : Proper G S c
• into : Into S c P
• card (i : ℕ) : i ∈ P → (cls S c i).card = s

structure HajnalSzemeredi.IsNear {V : Type u_1} (G : SimpleGraph V) (S : Finset V) (P : Finset ℕ) (c : V → ℕ) (s lo hi : ℕ) : Prop

Coloración casi equitativa: todas las clases de tamaño s, salvo una clase pequeña lo de tamaño s - 1 y una clase grande hi de tamaño s + 1.

• proper : Proper G S c
• into : Into S c P
• lo_mem : lo ∈ P
• hi_mem : hi ∈ P
• lo_ne_hi : lo ≠ hi
• card_lo : (cls S c lo).card + 1 = s
• card_hi : (cls S c hi).card = s + 1
• card (i : ℕ) : i ∈ P → i ≠ lo → i ≠ hi → (cls S c i).card = s

def HajnalSzemeredi.Movable {V : Type u_1} (G : SimpleGraph V) (S : Finset V) (c : V → ℕ) (v : V) (j : ℕ) : Prop

v es movible a la clase j: no tiene vecinos en ella.

Equations

• HajnalSzemeredi.Movable G S c v j = ∀ w ∈ HajnalSzemeredi.cls S c j, ¬G.Adj v w

def HajnalSzemeredi.Mov {V : Type u_1} (G : SimpleGraph V) (S : Finset V) (c : V → ℕ) (i j : ℕ) : Prop

Arco i → j del digrafo auxiliar H(G, c): algún vértice de la clase i es movible a j.

Equations

• HajnalSzemeredi.Mov G S c i j = ∃ v ∈ HajnalSzemeredi.cls S c i, HajnalSzemeredi.Movable G S c v j

noncomputable def HajnalSzemeredi.acc {V : Type u_1} (G : SimpleGraph V) (S : Finset V) (P : Finset ℕ) (c : V → ℕ) (lo : ℕ) : Finset ℕ

Clases accesibles: las que alcanzan a lo en H(G, c).

Equations

• HajnalSzemeredi.acc G S P c lo = {i ∈ P | Relation.ReflTransGen (HajnalSzemeredi.Mov G S c) i lo}

Lemas básicos sobre clases

@[simp]

theorem HajnalSzemeredi.mem_cls {V : Type u_1} {S : Finset V} {c : V → ℕ} {i : ℕ} {v : V} : v ∈ cls S c i ↔ v ∈ S ∧ c v = i

theorem HajnalSzemeredi.cls_subset {V : Type u_1} (S : Finset V) (c : V → ℕ) (i : ℕ) : cls S c i ⊆ S

@[simp]

theorem HajnalSzemeredi.mem_nbr {V : Type u_1} {G : SimpleGraph V} {S : Finset V} {v w : V} : w ∈ nbr G S v ↔ w ∈ S ∧ G.Adj v w

theorem HajnalSzemeredi.cls_disjoint {V : Type u_1} {S : Finset V} {c : V → ℕ} {i j : ℕ} (h : i ≠ j) : Disjoint (cls S c i) (cls S c j)

theorem HajnalSzemeredi.sum_card_cls {V : Type u_1} {S : Finset V} {c : V → ℕ} {P : Finset ℕ} (h : Into S c P) : ∑ i ∈ P, (cls S c i).card = S.card

Las clases de la paleta particionan S: la suma de sus tamaños es |S|.

Mover un vértice a otra clase

theorem HajnalSzemeredi.cls_update_self {V : Type u_1} {S : Finset V} {c : V → ℕ} {v : V} {j : ℕ} (hv : v ∈ S) : cls S (Function.update c v j) j = insert v (cls S c j)

theorem HajnalSzemeredi.cls_update_old {V : Type u_1} {S : Finset V} {c : V → ℕ} {v : V} {j : ℕ} (hj : c v ≠ j) : cls S (Function.update c v j) (c v) = (cls S c (c v)).erase v

theorem HajnalSzemeredi.cls_update_other {V : Type u_1} {S : Finset V} {c : V → ℕ} {v : V} {j k : ℕ} (hk : k ≠ j) (hk' : k ≠ c v) : cls S (Function.update c v j) k = cls S c k

theorem HajnalSzemeredi.card_cls_update_self {V : Type u_1} {S : Finset V} {c : V → ℕ} {v : V} {j : ℕ} (hv : v ∈ S) (hj : c v ≠ j) : (cls S (Function.update c v j) j).card = (cls S c j).card + 1

theorem HajnalSzemeredi.card_cls_update_old {V : Type u_1} {S : Finset V} {c : V → ℕ} {v : V} {j : ℕ} (hv : v ∈ S) (hj : c v ≠ j) : (cls S (Function.update c v j) (c v)).card + 1 = (cls S c (c v)).card

theorem HajnalSzemeredi.into_update {V : Type u_1} {S : Finset V} {c : V → ℕ} {v : V} {j : ℕ} {P : Finset ℕ} (h : Into S c P) (hj : j ∈ P) : Into S (Function.update c v j) P

theorem HajnalSzemeredi.proper_update {V : Type u_1} {G : SimpleGraph V} {S : Finset V} {c : V → ℕ} {v : V} {j : ℕ} (h : Proper G S c) (hmov : Movable G S c v j) : Proper G S (Function.update c v j)

Mover un vértice movible preserva la propiedad.