@[reducible, inline]

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

Equations

• N χ i x = (SimpleGraph.EdgeLabelling.coloredNeighborSet i x).toFinset

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 W : Type} [LinearOrder W] {c : W} {f : V → W} {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 W : Type} [LinearOrder W] {f : V → W} {X : Finset V} [Nonempty { x : V // x ∈ X }] (v : { x : V // x ∈ X }) : mymin f X ≤ f ↑v

def lift {V : Type} {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} {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 lift_nonempty {V : Type} {X : Finset V} (X' : Finset { x : V // x ∈ X }) (nen : X'.Nonempty) : (lift X').Nonempty

theorem lift_subset {V : Type} {X : Finset V} (X' : Finset { x : V // x ∈ X }) : lift X' ⊆ X

theorem lift_card {V : Type} {X : Finset V} (X' : Finset { x : V // x ∈ X }) : X'.card = (lift X').card

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

def ppY {V : Type} {r : ℕ} [DecidableEq V] [Fintype V] (χ : SimpleGraph.TopEdgeLabelling V (Fin r)) (X : Finset V) (Y : Fin r → Finset V) (i : Fin r) : ℕ

Equations

• ppY χ X Y i = if h : X.Nonempty then (Finset.image (fun (x : V) => (N χ i x ∩ Y i).card) X).min' ⋯ else 0

noncomputable def p'p {V : Type} {r : ℕ} [DecidableEq V] [Fintype V] (χ : SimpleGraph.TopEdgeLabelling V (Fin r)) (X : Finset V) (Y : Fin r → Finset V) (i : Fin r) : ℝ

Equations

• p'p χ X Y i = ↑(ppY χ X Y i) / ↑(Y i).card

structure Saga {V : Type} {r : ℕ} (χ : SimpleGraph.TopEdgeLabelling V (Fin r)) : Type

• X : Finset V
• Y : Fin r → Finset V

@[reducible, inline]

abbrev Saga.pY {V : Type} {r : ℕ} [DecidableEq V] [Fintype V] {χ : SimpleGraph.TopEdgeLabelling V (Fin r)} (ki : Saga χ) (i : Fin r) : ℕ

Equations

• ki.pY i = ppY χ ki.X ki.Y i

@[reducible, inline]

noncomputable abbrev Saga.p {V : Type} {r : ℕ} [DecidableEq V] [Fintype V] {χ : SimpleGraph.TopEdgeLabelling V (Fin r)} (ki : Saga χ) (i : Fin r) : ℝ

Equations

• ki.p i = p'p χ ki.X ki.Y i

theorem pk_le_one {V : Type} {r : ℕ} [DecidableEq V] [Fintype V] {χ : SimpleGraph.TopEdgeLabelling V (Fin r)} (ki : Saga χ) (i : Fin r) : ki.p i ≤ 1

theorem p_monoX {V : Type} {r : ℕ} [DecidableEq V] [Fintype V] (χ : SimpleGraph.TopEdgeLabelling V (Fin r)) {X X' : Finset V} (xsub : X' ⊆ X) (h : X'.Nonempty) (Y : Fin r → Finset V) (i : Fin r) : p'p χ X Y i ≤ p'p χ X' Y i

theorem p_monoY {V : Type} {r : ℕ} [DecidableEq V] [Fintype V] (χ : SimpleGraph.TopEdgeLabelling V (Fin r)) {X : Finset V} (Y Y' : Fin r → Finset V) (h : ∀ (i : Fin r), Y' i ⊆ Y i) (i : Fin r) : p'p χ X Y i ≤ p'p χ X Y' i

theorem pk_le_mem {V : Type} {r : ℕ} [DecidableEq V] [Fintype V] {χ : SimpleGraph.TopEdgeLabelling V (Fin r)} {x : V} {ki : Saga χ} (i : Fin r) (xin : x ∈ ki.X) : ki.pY i ≤ (N χ i x ∩ ki.Y i).card

theorem nonempty_of_ppos {V : Type} {r : ℕ} [DecidableEq V] [Fintype V] {χ : SimpleGraph.TopEdgeLabelling V (Fin r)} {ki : Saga χ} (ppos : ∀ (i : Fin r), 0 < ki.pY i) : Nonempty { x : V // x ∈ ki.X }

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