theorem Real.pow_le_rpow_of_exponent_ge {x : ℝ} {y z : ℕ} (hx0 : 0 ≤ x) (hx1 : x ≤ 1) (hyz : z ≤ y) : x ^ y ≤ x ^ z

theorem Finset.card_le_card_insert {α : Type u_1} [DecidableEq α] (a : α) (s : Finset α) : s.card ≤ (insert a s).card

theorem erm {R : Type u_1} [CommMonoidWithZero R] [PartialOrder R] [ZeroLEOneClass R] [PosMulMono R] {L : Type u_3} {f : L → R} {r : R} {t : List L} (hf0 : ∀ x ∈ t, 0 ≤ f x) (hf : ∀ x ∈ t, r ≤ f x) : r ^ t.length ≤ (List.map f t).prod

theorem reh {V : Type} [Fintype V] [DecidableEq V] [Nonempty V] (Y : Finset V) : Membership.mem Y.val = ↑Y

theorem pk_subset {V : Type} {r : ℕ} [Fintype V] [DecidableEq V] [Nonempty V] [Nonempty (Fin r)] {χ : SimpleGraph.TopEdgeLabelling V (Fin r)} {X' : Finset V} (nen : X'.Nonempty) (ki : Saga χ) (sub : X' ⊆ ki.X) (i : Fin r) : ki.p i ≤ p'p χ X' ki.Y i

structure BookParams (V : Type) (r : ℕ) [Fintype V] [DecidableEq V] [Nonempty V] [Nonempty (Fin r)] : Type

• t : ℕ
• tpos : 0 < self.t
• Λ₀ : ℝ
• Λ₀ge : -1 ≤ self.Λ₀
• δ : ℝ
• δpos : 0 < self.δ
• χ : SimpleGraph.TopEdgeLabelling V (Fin r)
• s : Saga self.χ
• nen : self.s.X.Nonempty
• pYpos (i : Fin r) : 0 < self.s.pY i
• lle : self.Λ₀ ≤ ↑self.t
• δle : self.δ ≤ 1 / 4
• tge : 2 ≤ self.t
• pnn : 0 ≤ (Finset.image self.s.p Finset.univ).min' ⋯ - 3 * self.δ / 4

noncomputable def BookParams.p₀ {V : Type} {r : ℕ} [Fintype V] [DecidableEq V] [Nonempty V] [Nonempty (Fin r)] (param : BookParams V r) : ℝ

Equations

• param.p₀ = (Finset.image param.s.p Finset.univ).min' ⋯

noncomputable def BookParams.δp {V : Type} {r : ℕ} [Fintype V] [DecidableEq V] [Nonempty V] [Nonempty (Fin r)] (param : BookParams V r) : ℝ

Equations

• param.δp = param.p₀ - 3 * param.δ / 4

theorem tpos {V : Type} {r : ℕ} [Fintype V] [DecidableEq V] [Nonempty V] [Nonempty (Fin r)] {param : BookParams V r} : 0 ≤ 1 - 1 / ↑param.t

theorem p₀pos {V : Type} {r : ℕ} [Fintype V] [DecidableEq V] [Nonempty V] [Nonempty (Fin r)] {param : BookParams V r} : 0 ≤ param.p₀

theorem p₀le {V : Type} {r : ℕ} [Fintype V] [DecidableEq V] [Nonempty V] [Nonempty (Fin r)] {param : BookParams V r} {i : Fin r} : param.p₀ ≤ param.s.p i

theorem δppos {V : Type} {r : ℕ} [Fintype V] [DecidableEq V] [Nonempty V] [Nonempty (Fin r)] {param : BookParams V r} : 0 ≤ param.δp

structure KeyIn {V : Type} {r : ℕ} [Fintype V] [DecidableEq V] [Nonempty V] [Nonempty (Fin r)] (param : BookParams V r) extends Saga param.χ : Type

• X : Finset V
• Y : Fin r → Finset V
• pYpos (i : Fin r) : 0 < self.pY i
• mono {i : Fin r} : param.s.p i ≤ self.p i

theorem p'_le_one {V : Type} {r : ℕ} [Fintype V] [DecidableEq V] [Nonempty V] [Nonempty (Fin r)] {param : BookParams V r} (kin : KeyIn param) (i : Fin r) : kin.p i ≤ 1

noncomputable def KeyIn.α {V : Type} {r : ℕ} [Fintype V] [DecidableEq V] [Nonempty V] [Nonempty (Fin r)] {param : BookParams V r} (kin : KeyIn param) (i : Fin r) : ℝ

Equations

• kin.α i = 1 / ↑param.t * (kin.p i - param.p₀ + param.δ)

theorem αpos {V : Type} {r : ℕ} [Fintype V] [DecidableEq V] [Nonempty V] [Nonempty (Fin r)] {param : BookParams V r} (kin : KeyIn param) (i : Fin r) : 0 < kin.α i

noncomputable def β (r : ℕ) : ℝ

Equations

• β r = 3 ^ (-4 * ↑r)

noncomputable def C (r : ℕ) : ℝ

Equations

• C r = 4 * ↑r * √↑r

theorem βpos {r : ℕ} [Nonempty (Fin r)] : 0 < β r

theorem βposr {r : ℕ} [Nonempty (Fin r)] : 0 < β r / ↑r

structure KeyOut {V : Type} {r : ℕ} [Fintype V] [DecidableEq V] [Nonempty V] [Nonempty (Fin r)] {param : BookParams V r} (bin : KeyIn param) extends Saga param.χ : Type

• X : Finset V
• Y : Fin r → Finset V
• l : Fin r
• Λ : ℝ
• Λge : -1 ≤ self.Λ
• x : V
• xX : self.x ∈ bin.X
• X'sub : self.X ⊆ bin.X
• Y'sub (i : Fin r) : self.Y i ⊆ N param.χ i self.x ∩ bin.Y i
• βcard : β r * Real.exp (-C r * √(self.Λ + 1)) * ↑bin.X.card ≤ ↑self.X.card
• Y'card (i : Fin r) : ↑(self.Y i).card = bin.p i * ↑(bin.Y i).card
• f : bin.p self.l + self.Λ * bin.α self.l ≤ self.p self.l
• g (i : Fin r) : i ≠ self.l → bin.p i - bin.α i ≤ self.p i
• nen : self.X.Nonempty

noncomputable def keybi {V : Type} {r : ℕ} [Fintype V] [DecidableEq V] [Nonempty V] [Nonempty (Fin r)] {param : BookParams V r} (bin : KeyIn param) : KeyOut bin

Equations

• One or more equations did not get rendered due to their size.

noncomputable def ε {V : Type} {r : ℕ} [Fintype V] [DecidableEq V] [Nonempty V] [Nonempty (Fin r)] (param : BookParams V r) : ℕ → ℝ

Equations

• ε param r = β r / ↑r * Real.exp (-C r * √(param.Λ₀ + 1))

noncomputable def Xb {V : Type} {r : ℕ} [Fintype V] [DecidableEq V] [Nonempty V] [Nonempty (Fin r)] (param : BookParams V r) (Λs : Fin r → List ℝ) (T : Fin r → Finset V) (i : Fin r) : ℝ

Equations

• Xb param Λs T i = ε param r ^ (r * (T i).card + (Λs i).length) * Real.exp (-4 * ↑r * √↑r * (List.map (fun (Λ : ℝ) => √(1 + Λ)) (Λs i)).sum) * ↑param.s.X.card - ↑r * ↑(T i).card

theorem εpos {V : Type} {r : ℕ} [Fintype V] [DecidableEq V] [Nonempty V] [Nonempty (Fin r)] {param : BookParams V r} {t : ℕ} : 0 ≤ ε param t

theorem εle1 {V : Type} {r : ℕ} [Fintype V] [DecidableEq V] [Nonempty V] [Nonempty (Fin r)] {param : BookParams V r} {t : ℕ} : ε param t ≤ 1

theorem εleβ {V : Type} {r : ℕ} [Fintype V] [DecidableEq V] [Nonempty V] [Nonempty (Fin r)] {param : BookParams V r} {t : ℕ} : ε param r ≤ β r

structure BookIn {V : Type} {r : ℕ} [Fintype V] [DecidableEq V] [Nonempty V] [Nonempty (Fin r)] (param : BookParams V r) extends KeyIn param : Type

• X : Finset V
• Y : Fin r → Finset V
• pYpos (i : Fin r) : 0 < self.pY i
• mono {i : Fin r} : param.s.p i ≤ self.p i
• T : Fin r → Finset V
• Tle (i : Fin r) : (self.T i).card ≤ param.t
• Tdisj (i : Fin r) : Disjoint self.X (self.T i)
• Λs : Fin r → List ℝ
• Λsge (i : Fin r) (Λ : ℝ) : Λ ∈ self.Λs i → param.Λ₀ < Λ
• l41 (i : Fin r) : param.δ * ((1 - 1 / ↑param.t) ^ (self.T i).card * (List.map (fun (Λ : ℝ) => 1 + Λ / ↑param.t) (self.Λs i)).prod) ≤ self.p i - param.p₀ + param.δ
• l44 (i : Fin r) : param.δp ^ ((self.T i).card + (self.Λs i).length) * ↑(param.s.Y i).card ≤ ↑(self.Y i).card
• l45 (i : Fin r) : Xb param self.Λs self.T i ≤ ↑self.X.card
• rainbow (i : Fin r) (y : V) : y ∈ self.T i → ∀ x ∈ self.X, x ∈ N param.χ i y
• mbook (i : Fin r) : SimpleGraph.TopEdgeLabelling.MonochromaticBook i (self.T i) (self.Y i)

noncomputable def BookParams.bin {V : Type} {r : ℕ} [Fintype V] [DecidableEq V] [Nonempty V] [Nonempty (Fin r)] (param : BookParams V r) : BookIn param

Equations

• One or more equations did not get rendered due to their size.

def BookIn.maxB {V : Type} {r : ℕ} [Fintype V] [DecidableEq V] [Nonempty V] [Nonempty (Fin r)] {param : BookParams V r} (bin : BookIn param) : ℕ

Equations

• bin.maxB = ∑ i : Fin r, (bin.Λs i).length

noncomputable def BookIn.maxT {V : Type} {r : ℕ} [Fintype V] [DecidableEq V] [Nonempty V] [Nonempty (Fin r)] {param : BookParams V r} (bin : BookIn param) : ℕ

Equations

• bin.maxT = ∑ i : Fin r, (bin.T i).card

def BookIn.B {V : Type} {r : ℕ} [Fintype V] [DecidableEq V] [Nonempty V] [Nonempty (Fin r)] {param : BookParams V r} (re : BookIn param) : Fin r → ℕ

Equations

• re.B i = (re.Λs i).length

def BookIn.C {V : Type} {r : ℕ} [Fintype V] [DecidableEq V] [Nonempty V] [Nonempty (Fin r)] {param : BookParams V r} (re : BookIn param) : Fin r → ℕ

Equations

• re.C i = (re.T i).card

noncomputable def BookIn.Xbound {V : Type} {r : ℕ} [Fintype V] [DecidableEq V] [Nonempty V] [Nonempty (Fin r)] {param : BookParams V r} (bin : BookIn param) (T : Fin r → Finset V) (i : Fin r) : ℝ

Equations

• bin.Xbound T i = Xb param bin.Λs T i

theorem Xbound_pos {V : Type} {r : ℕ} [Fintype V] [DecidableEq V] [Nonempty V] [Nonempty (Fin r)] {param : BookParams V r} {bin : BookIn param} {T : Fin r → Finset V} {i : Fin r} : 0 < bin.Xbound T i

structure BookOut {V : Type} {r : ℕ} [Fintype V] [DecidableEq V] [Nonempty V] [Nonempty (Fin r)] (param : BookParams V r) (maxT : ℕ) : Type

• bin : BookIn param
• step_inc : maxT < self.bin.maxT

def newYb {V : Type} {r : ℕ} [Fintype V] [DecidableEq V] [Nonempty V] [Nonempty (Fin r)] {param : BookParams V r} {bin : BookIn param} (kout : KeyOut bin.toKeyIn) (i : Fin r) : Finset V

Equations

• newYb kout i = if i = kout.l then kout.Y i else bin.Y i

def newY {V : Type} {r : ℕ} [Fintype V] [DecidableEq V] [Nonempty V] [Nonempty (Fin r)] {param : BookParams V r} {bin : BookIn param} (kout : KeyOut bin.toKeyIn) (i j : Fin r) : Finset V

Equations

• newY kout i j = if i = j then kout.Y i else bin.Y i

def newT {V : Type} {r : ℕ} [Fintype V] [DecidableEq V] [Nonempty V] [Nonempty (Fin r)] {param : BookParams V r} {bin : BookIn param} (i j : Fin r) (x : V) : Finset V

Equations

• newT i j x = if i = j then insert x (bin.T i) else bin.T i

theorem l42p {V : Type} {r : ℕ} [Fintype V] [DecidableEq V] [Nonempty V] [Nonempty (Fin r)] {param : BookParams V r} (bin : BookIn param) (i : Fin r) : param.δp ≤ bin.p i

theorem pl1 {V : Type} {r : ℕ} [Fintype V] [DecidableEq V] [Nonempty V] [Nonempty (Fin r)] {param : BookParams V r} (bin : BookIn param) (i : Fin r) : param.δp ≤ 1

theorem l42α {V : Type} {r : ℕ} [Fintype V] [DecidableEq V] [Nonempty V] [Nonempty (Fin r)] {param : BookParams V r} (bin : BookIn param) (i : Fin r) : param.δ / (4 * ↑param.t) ≤ bin.α i

noncomputable def BookParams.B {V : Type} {r : ℕ} [Fintype V] [DecidableEq V] [Nonempty V] [Nonempty (Fin r)] {param : BookParams V r} : ℕ

Equations

• BookParams.B = ⌈↑param.t * (4 * Real.log (1 / param.δ)) / param.Λ₀⌉₊

theorem l43 {V : Type} {r : ℕ} [Fintype V] [DecidableEq V] [Nonempty V] [Nonempty (Fin r)] {param : BookParams V r} (bin : BookIn param) (i : Fin r) : bin.B i ≤ BookParams.B

theorem l44color {V : Type} {r : ℕ} [Fintype V] [DecidableEq V] [Nonempty V] [Nonempty (Fin r)] {param : BookParams V r} {bin : BookIn param} {x : V} (kout : KeyOut bin.toKeyIn) (j : Fin r) (ghrm : x ∉ bin.T j) : have newY := fun (i : Fin r) => if i = j then kout.Y i else bin.Y i; have newT := fun (i : Fin r) => if i = j then insert x (bin.T i) else bin.T i; ∀ (i : Fin r), param.δp ^ ((newT i).card + bin.B i) * ↑(param.s.Y i).card ≤ ↑(newY i).card

theorem l44boost {V : Type} {r : ℕ} [Fintype V] [DecidableEq V] [Nonempty V] [Nonempty (Fin r)] {param : BookParams V r} {bin : BookIn param} {kout : KeyOut bin.toKeyIn} : have newΛs := fun (i : Fin r) => if i = kout.l then kout.Λ :: bin.Λs i else bin.Λs i; ∀ (i : Fin r), param.δp ^ ((bin.T i).card + (newΛs i).length) * ↑(param.s.Y i).card ≤ ↑(newYb kout i).card

theorem l45boost {V : Type} {r : ℕ} [Fintype V] [DecidableEq V] [Nonempty V] [Nonempty (Fin r)] {param : BookParams V r} {bin : BookIn param} {kout : KeyOut bin.toKeyIn} : have newΛs := fun (i : Fin r) => if i = kout.l then kout.Λ :: bin.Λs i else bin.Λs i; ∀ (i : Fin r), Xb param newΛs bin.T i ≤ ↑kout.X.card

theorem l45color {V : Type} {r : ℕ} [Fintype V] [DecidableEq V] [Nonempty V] [Nonempty (Fin r)] {param : BookParams V r} {bin : BookIn param} (kout : KeyOut bin.toKeyIn) (j : Fin r) (jn : j ≠ kout.l) : have X' := N param.χ j kout.x ∩ kout.X; have newT := fun (i : Fin r) => if i = j then insert kout.x (bin.T i) else bin.T i; ∀ (i : Fin r), bin.Xbound newT i ≤ ↑X'.card

theorem l41nothing {V : Type} {r : ℕ} [Fintype V] [DecidableEq V] [Nonempty V] [Nonempty (Fin r)] {param : BookParams V r} {bin : BookIn param} (X' : Finset V) (X'sub : X' ⊆ bin.X) (i : Fin r) (nen : X'.Nonempty) : param.δ * ((1 - 1 / ↑param.t) ^ (bin.T i).card * (List.map (fun (Λ : ℝ) => 1 + Λ / ↑param.t) (bin.Λs i)).prod) ≤ p'p param.χ X' bin.Y i - param.p₀ + param.δ

theorem l41color {V : Type} {r : ℕ} [Fintype V] [DecidableEq V] [Nonempty V] [Nonempty (Fin r)] {param : BookParams V r} {bin : BookIn param} {kout : KeyOut bin.toKeyIn} (j : Fin r) (Tne : kout.x ∉ bin.T j) (jnn : j ≠ kout.l) (nen : (N param.χ j kout.x ∩ kout.X).Nonempty) : have X' := N param.χ j kout.x ∩ kout.X; have newY := fun (i : Fin r) => if i = j then kout.Y i else bin.Y i; have newT := fun (i : Fin r) => if i = j then insert kout.x (bin.T i) else bin.T i; ∀ (i : Fin r), param.δ * ((1 - 1 / ↑param.t) ^ (newT i).card * (List.map (fun (Λ : ℝ) => 1 + Λ / ↑param.t) (bin.Λs i)).prod) ≤ p'p param.χ X' newY i - param.p₀ + param.δ

theorem l41boost {V : Type} {r : ℕ} [Fintype V] [DecidableEq V] [Nonempty V] [Nonempty (Fin r)] {param : BookParams V r} {bin : BookIn param} {kout : KeyOut bin.toKeyIn} : have newΛs := fun (i : Fin r) => if i = kout.l then kout.Λ :: bin.Λs i else bin.Λs i; ∀ (i : Fin r), param.δ * ((1 - 1 / ↑param.t) ^ (bin.T i).card * (List.map (fun (Λ : ℝ) => 1 + Λ / ↑param.t) (newΛs i)).prod) ≤ p'p param.χ kout.X (newYb kout) i - param.p₀ + param.δ

theorem l46 {V : Type} {r : ℕ} [Fintype V] [DecidableEq V] [Nonempty V] [Nonempty (Fin r)] {param : BookParams V r} {bin : BookIn param} {i : Fin r} : (List.map (fun (Λ : ℝ) => √(1 + Λ)) (bin.Λs i)).sum ≤ ↑param.t * 7 * ↑r * Real.log (1 / param.δ) / √param.Λ₀