theorem mau {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) : Disjoint (bin.T i) (kout.Y i)

theorem mono_boost {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) : SimpleGraph.TopEdgeLabelling.MonochromaticBook i (bin.T i) (newYb kout i)

theorem mono {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} (i : Fin r) : have Y' := 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; SimpleGraph.TopEdgeLabelling.MonochromaticBook i (newT i) (Y' i)

theorem pyposcolor {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} : have X' := N param.χ j kout.x ∩ kout.X; have Y' := fun (i : Fin r) => if i = j then kout.Y i else bin.Y i; ∀ (i : Fin r), 0 < { X := X', Y := Y' }.pY i

theorem pypos {V : Type} {r : ℕ} [Fintype V] [DecidableEq V] [Nonempty V] [Nonempty (Fin r)] {param : BookParams V r} {bin : BookIn param} {kout : KeyOut bin.toKeyIn} {χ : SimpleGraph.TopEdgeLabelling V (Fin r)} : have X' := kout.X; have Y' := fun (i : Fin r) => if i = kout.l then kout.Y i else bin.Y i; ∀ {i : Fin r}, 0 < { X := X', Y := Y' }.pY i

theorem choice_j {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), j ≠ kout.l ∧ (N param.χ j kout.x ∩ kout.X).card ≤ (kout.X.card - 1) / r

@[irreducible]

noncomputable def step {V : Type} {r : ℕ} [Fintype V] [DecidableEq V] [Nonempty V] [Nonempty (Fin r)] {param : BookParams V r} (bin : BookIn param) (Tlt : ∀ (i : Fin r), (bin.T i).card < param.t) : BookOut param (∑ i : Fin r, (bin.T i).card)

Equations

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

@[irreducible]

noncomputable def stepper {V : Type} {r : ℕ} [Fintype V] [DecidableEq V] [Nonempty V] [Nonempty (Fin r)] {param : BookParams V r} (bin : BookIn param) : ∃ (sn : BookIn param) (j : Fin r), param.t = (sn.T j).card ∧ param.δp ^ (param.t + BookParams.B) * ↑(param.s.Y j).card ≤ ↑(sn.Y j).card

Equations

• ⋯ = ⋯

theorem book {V : Type} {r : ℕ} [Fintype V] [DecidableEq V] [Nonempty V] [Nonempty (Fin r)] (t m : ℕ) (χ : SimpleGraph.TopEdgeLabelling V (Fin r)) (tpos : 0 < t) (mpos : 0 < m) (X : Finset V) (Y : Fin r → Finset V) (p : ℝ) (ppos : 0 < p) (μ : ℝ) (μge : 2 ^ 10 * ↑r ^ 3 ≤ μ) (tge : μ ^ 5 / p ≤ ↑t) (Y'card : ∀ (i : Fin r) (x : V), p * ↑(Y i).card ≤ ↑(N χ i x ∩ Y i).card) (Xge : (μ ^ 2 / p) ^ (μ * ↑r * ↑t) ≤ ↑X.card) (Yge : ∀ (i : Fin r), Real.exp (2 ^ 13 * ↑r ^ 3 / μ ^ 2) ^ t * ↑m ≤ ↑(Y i).card) : ∃ (c : Fin r) (T : Finset V) (M : Finset V), T.card = t ∧ m ≤ M.card ∧ SimpleGraph.TopEdgeLabelling.MonochromaticBook c T M