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

Estructura de una coloración casi equitativa con clase grande inaccesible

Contexto (Ctx): c es casi equitativa en S con paleta P (|P| = r + 1), grado máximo ≤ r, y la clase grande hi no es accesible. Sea 𝒜 = acc la familia de clases accesibles y ℬ = P \ 𝒜.

• h21: todo y ∈ B tiene un vecino en cada clase de 𝒜 (desigualdad (2.1));
• card_B, card_A: |B| = |ℬ| s + 1, |A| + 1 = |𝒜| s;
• two_le_card_acc: |𝒜| ≥ 2;
• clases terminales y la familia 𝒜' = T_U (exists_TU), con la propiedad (2.2);
• countHyp: las hipótesis de la parte de conteo.

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

Contexto del lema principal.

• near : IsNear G S P c s lo hi
• deg : DegLe G S r
• card_P : P.card = r + 1
• hi_not : hi ∉ acc G S P c lo

def HajnalSzemeredi.avoid {V : Type u_1} (G : SimpleGraph V) (S : Finset V) (c : V → ℕ) (W a b : ℕ) : Prop

Arcos de H - W.

Equations

• HajnalSzemeredi.avoid G S c W a b = (HajnalSzemeredi.Mov G S c a b ∧ a ≠ W ∧ b ≠ W)

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

T_W: clases accesibles distintas de W que no alcanzan lo en H - W.

Equations

• HajnalSzemeredi.T G S P c lo W = {X ∈ (HajnalSzemeredi.acc G S P c lo).erase W | ¬Relation.ReflTransGen (HajnalSzemeredi.avoid G S c W) X lo}

theorem HajnalSzemeredi.card_part {V : Type u_1} (S : Finset V) (c : V → ℕ) (Q : Finset ℕ) : (part S c Q).card = ∑ i ∈ Q, (cls S c i).card

theorem HajnalSzemeredi.split_avoid {α : Type u_2} {R : α → α → Prop} {x z a : α} : Relation.ReflTransGen R a z → a ≠ x → Relation.ReflTransGen (fun (u v : α) => R u v ∧ u ≠ x ∧ v ≠ x) a z ∨ Relation.ReflTransGen R x z

x ∈ T y x alcanza un objetivo: si el camino pasa por x', o lo evita o x' alcanza.

theorem HajnalSzemeredi.rtgMono {α : Type u_2} {R R' : α → α → Prop} {a b : α} (h : Relation.ReflTransGen R a b) (hR : ∀ (x y : α), R x y → R' x y) : Relation.ReflTransGen R' a b

Transport reachability along inclusion of relations.

theorem HajnalSzemeredi.Ctx.acc_subset {V : Type u_1} {G : SimpleGraph V} {S : Finset V} {P : Finset ℕ} {c : V → ℕ} {lo : ℕ} : acc G S P c lo ⊆ P

theorem HajnalSzemeredi.Ctx.lo_mem_acc {V : Type u_1} {G : SimpleGraph V} {S : Finset V} {P : Finset ℕ} {c : V → ℕ} {r s lo hi : ℕ} (h : Ctx G S P c r s lo hi) : lo ∈ acc G S P c lo

theorem HajnalSzemeredi.Ctx.mem_acc_of_mov {V : Type u_1} {G : SimpleGraph V} {S : Finset V} {P : Finset ℕ} {c : V → ℕ} {r s lo hi : ℕ} (h : Ctx G S P c r s lo hi) {a b : ℕ} (hab : Mov G S c a b) (hb : b ∈ acc G S P c lo) : a ∈ acc G S P c lo

theorem HajnalSzemeredi.Ctx.hi_mem_B {V : Type u_1} {G : SimpleGraph V} {S : Finset V} {P : Finset ℕ} {c : V → ℕ} {r s lo hi : ℕ} (h : Ctx G S P c r s lo hi) : hi ∈ P \ acc G S P c lo

theorem HajnalSzemeredi.Ctx.cover {V : Type u_1} {G : SimpleGraph V} {S : Finset V} {P : Finset ℕ} {c : V → ℕ} {r s lo hi : ℕ} (h : Ctx G S P c r s lo hi) (v : V) : v ∈ S → c v ∈ acc G S P c lo ∪ P \ acc G S P c lo

theorem HajnalSzemeredi.Ctx.card_r {V : Type u_1} {G : SimpleGraph V} {S : Finset V} {P : Finset ℕ} {c : V → ℕ} {r s lo hi : ℕ} (h : Ctx G S P c r s lo hi) : r + 1 = (acc G S P c lo).card + (P \ acc G S P c lo).card

theorem HajnalSzemeredi.Ctx.h21 {V : Type u_1} {G : SimpleGraph V} {S : Finset V} {P : Finset ℕ} {c : V → ℕ} {r s lo hi : ℕ} (h : Ctx G S P c r s lo hi) {y : V} (hy : y ∈ part S c (P \ acc G S P c lo)) {X : ℕ} (hX : X ∈ acc G S P c lo) : (nIn G S c y X).Nonempty

(2.1): todo vértice de B tiene un vecino en cada clase accesible.

theorem HajnalSzemeredi.Ctx.card_B {V : Type u_1} {G : SimpleGraph V} {S : Finset V} {P : Finset ℕ} {c : V → ℕ} {r s lo hi : ℕ} (h : Ctx G S P c r s lo hi) : (part S c (P \ acc G S P c lo)).card = (P \ acc G S P c lo).card * s + 1

theorem HajnalSzemeredi.Ctx.card_A {V : Type u_1} {G : SimpleGraph V} {S : Finset V} {P : Finset ℕ} {c : V → ℕ} {r s lo hi : ℕ} (h : Ctx G S P c r s lo hi) : (part S c (acc G S P c lo)).card + 1 = (acc G S P c lo).card * s

theorem HajnalSzemeredi.Ctx.two_le_card_acc {V : Type u_1} {G : SimpleGraph V} {S : Finset V} {P : Finset ℕ} {c : V → ℕ} {r s lo hi : ℕ} (h : Ctx G S P c r s lo hi) : 2 ≤ (acc G S P c lo).card

|𝒜| ≥ 2.

theorem HajnalSzemeredi.Ctx.lo_notMem_T {V : Type u_1} {G : SimpleGraph V} {S : Finset V} {P : Finset ℕ} {c : V → ℕ} {lo : ℕ} (W : ℕ) : lo ∉ T G S P c lo W

lo no está en ningún T_W.

theorem HajnalSzemeredi.Ctx.T_lo_nonempty {V : Type u_1} {G : SimpleGraph V} {S : Finset V} {P : Finset ℕ} {c : V → ℕ} {r s lo hi : ℕ} (h : Ctx G S P c r s lo hi) : (T G S P c lo lo).Nonempty

theorem HajnalSzemeredi.Ctx.exists_TU {V : Type u_1} {G : SimpleGraph V} {S : Finset V} {P : Finset ℕ} {c : V → ℕ} {r s lo hi : ℕ} (h : Ctx G S P c r s lo hi) : ∃ U ∈ acc G S P c lo, (T G S P c lo U).Nonempty ∧ (∀ W ∈ T G S P c lo U, ∀ X ∈ (acc G S P c lo).erase W, Relation.ReflTransGen (avoid G S c W) X lo) ∧ ∀ X ∈ T G S P c lo U, ∀ Y ∈ acc G S P c lo, Y ∉ T G S P c lo U → Y ≠ U → ¬Mov G S c X Y

Elección de U y de la familia 𝒜' = T_U.

theorem HajnalSzemeredi.Ctx.T_subset {V : Type u_1} {G : SimpleGraph V} {S : Finset V} {P : Finset ℕ} {c : V → ℕ} {lo : ℕ} (U : ℕ) : T G S P c lo U ⊆ (acc G S P c lo).erase U

theorem HajnalSzemeredi.Ctx.countHyp {V : Type u_1} {G : SimpleGraph V} {S : Finset V} {P : Finset ℕ} {c : V → ℕ} {r s lo hi : ℕ} (h : Ctx G S P c r s lo hi) {U : ℕ} (hU : U ∈ acc G S P c lo) (hne : (T G S P c lo U).Nonempty) (hP2 : ∀ X ∈ T G S P c lo U, ∀ Y ∈ acc G S P c lo, Y ∉ T G S P c lo U → Y ≠ U → ¬Mov G S c X Y) : CountHyp G S c (acc G S P c lo) (P \ acc G S P c lo) (T G S P c lo U) r s

Las hipótesis de conteo valen para 𝒜' = T_U.