MulticolorRamsey.RamseyBound

@[irreducible]

theorem ramseyNumber_le_pow {K : Type u_1} [Fintype K] [DecidableEq K] (n : K → ℕ) (hr : 2 ≤ Fintype.card K) :

theorem blo {r : ℕ} [Nonempty (Fin r)] {n : ℕ} {T M : Finset (Fin n)} {t k : ℕ} (χ : SimpleGraph.TopEdgeLabelling (Fin n) (Fin r)) (c : Fin r) (TMbook : SimpleGraph.TopEdgeLabelling.MonochromaticBook c T M) (Tcard : T.card = t) :

theorem lemma52 (n r : ℕ) (ε : ℝ) (εge : 0 < ε) (χ : SimpleGraph.TopEdgeLabelling (Fin n) (Fin r)) :

∃ (W : Finset (Fin n)) (S : Fin r → Finset (Fin n)), ↑n * ((1 + ε) / ↑r) ^ ∑ i : Fin r, (S i).card ≤ ↑W.card ∧ (∀ (i : Fin r) (w : Fin n), (1 / ↑r - ε) * ↑W.card - 1 ≤ ↑(N χ i w ∩ W).card) ∧ ∀ (i : Fin r), SimpleGraph.TopEdgeLabelling.MonochromaticBook i (S i) W

theorem lemma53r {r k : ℕ} (kge : 2 ≤ k) (rge : 2 ≤ r) {ε : ℝ} (εin : ε ∈ Set.Ioo 0 1) (s : Fin r → ℕ) (sk : ∀ (i : Fin r), s i ≤ k) :

have S := ∑ i : Fin r, s i; have b := Real.exp (-ε ^ 2 * ↑k / 2) * ↑r ^ (r * k) * ((1 + ε) / ↑r) ^ S; ε ^ 2 * ↑k ≤ ↑S → ↑(SimpleGraph.ramseyNumber fun (i : Fin r) => k - s i) ≤ b

theorem swap_ite_eq {K L : Type} [DecidableEq K] (c d : K) (t k : L) :

(fun (x : K) => if x = d then t else k) ∘ ⇑(Equiv.swap c d) = fun (x : K) => if x = c then t else k

theorem thm51r (r k : ℕ) (kp : 0 < k) (nr : 2 ≤ r) (kb : 2 ^ 160 * r ^ 16 ≤ k) :

have δ := 2 ^ (-160) * ↑r ^ (-12); have b := Real.exp (-δ * ↑k) * ↑r ^ (r * k); ↑(SimpleGraph.ramseyNumber fun (x : Fin r) => k) ≤ b