@[reducible, inline]

abbrev N {C : Type} {V : Type u_1} {G : SimpleGraph V} [DecidableRel G.Adj] [DecidableEq C] [Fintype V] (χ : SimpleGraph.EdgeColoring C) (i : C) (x : V) : Finset V

Equations

• N χ i x = SimpleGraph.EdgeColoring.coloredNeighborFinset i x

def mymin {V W : Type} [LinearOrder W] (f : V → W) (X : Finset V) [nen : Nonempty { x : V // x ∈ X }] : W

Equations

• mymin f X = (Finset.image f X).min' ⋯

theorem min_const {V : Type} {c : ℝ} {f : V → ℝ} {X : Finset V} (cn : ∀ x ∈ X, f x = c) [nen : Nonempty { x : V // x ∈ X }] : c = mymin f X

theorem min_le_ℕ {V : Type} {f : V → ℝ} {g : V → ℕ} {X : Finset V} [nen : Nonempty { x : V // x ∈ X }] (le : ∀ x ∈ X, f x ≤ ↑(g x)) : mymin f X ≤ ↑(mymin g X)

theorem min_le_mem_ℕ {V : Type} {f : V → ℕ} {X : Finset V} {v : { x : V // x ∈ X }} [Nonempty { x : V // x ∈ X }] : mymin f X ≤ f ↑v

def pY {r : ℕ} {V : Type} [Fintype V] [DecidableEq V] (X Y : Finset V) [nen : Nonempty { x : V // x ∈ X }] (χ : SimpleGraph.EdgeColoring (Fin r)) (i : Fin r) : ℕ

Equations

• pY X Y χ i = mymin (fun (x : V) => (N χ i x ∩ Y).card) X

noncomputable def p {r : ℕ} {V : Type} [Fintype V] [DecidableEq V] (X Y : Finset V) [Nonempty { x : V // x ∈ X }] (EC : SimpleGraph.EdgeColoring (Fin r)) (i : Fin r) : ℝ

Equations

• p X Y EC i = ↑(pY X Y EC i) / ↑Y.card

def lift {V : Type u_1} {X : Finset V} (X' : Finset { x : V // x ∈ X }) : Finset V

Equations

• lift X' = Finset.map (Function.Embedding.subtype fun (x : V) => x ∈ X) X'

instance lift.Nonempty {V : Type u_1} {X : Finset V} (X' : Finset { x : V // x ∈ X }) [nen : _root_.Nonempty { x : { x : V // x ∈ X } // x ∈ X' }] : _root_.Nonempty { x : V // x ∈ lift X' }

theorem tr {V : Type u_1} {X : Finset V} {X' : Finset { x : V // x ∈ X }} {p : V → Prop} (e : ∀ a ∈ X', p ↑a) (x : V) : x ∈ lift X' → p x

theorem key {r n : ℕ} [Nonempty (Fin r)] (V : Type) [DecidableEq V] [Nonempty V] [Fintype V] {cardV : Fintype.card V = n} (χ : SimpleGraph.EdgeColoring (Fin r)) (X : Finset V) [nenX : Nonempty { x : V // x ∈ X }] (Y : Fin r → Finset V) (Ypos : ∀ (i : Fin r), 0 < (Y i).card) (α : Fin r → ℝ) (αpos : ∀ (i : Fin r), 0 < α i) (ppos : ∀ (i : Fin r), 0 < pY X (Y i) χ i) : let β := 3 ^ (-4 * ↑r); let C := 4 * ↑r * √↑r; ∃ (l : Fin r) (Λ : ℝ), -1 ≤ Λ ∧ ∃ x ∈ X, ∃ (X' : Finset { x : V // x ∈ X }) (nx : Nonempty { x : { x : V // x ∈ X } // x ∈ X' }) (Y' : Fin r → Finset V), (∀ (i : Fin r), Y' i ⊆ N χ i x ∩ Y i) ∧ β * Real.exp (-C * √(Λ + 1)) * ↑X.card ≤ ↑X'.card ∧ (∀ (i : Fin r), i ≠ l → ↑(Y' i).card = p X (Y i) χ i * ↑(Y i).card) ∧ p X (Y l) χ l + Λ * α l ≤ p (lift X') (Y' l) χ l ∧ ∀ (i : Fin r), i ≠ l → p X (Y i) χ i - α i ≤ p (lift X') (Y' i) χ i