def LovaszLocalLemma.IsMulticolored (k : ℕ) (c : ℝ → Fin k) (T : Set ℝ) : Prop

The coloring $c : \mathbb{R} \to \text{Fin}\ k$ is multicolored on the set $T$ if every color $i \in \text{Fin}\ k$ is attained by some $x \in T$.

def LovaszLocalLemma.translate (S : Set ℝ) (t : ℝ) : Set ℝ

The translate of $S \subseteq \mathbb{R}$ by $t$, i.e. $S + t = \{s + t : s \in S\}$.

def LovaszLocalLemma.goodColorings (k : ℕ) (S : Finset ℝ) (t : ℝ) : Set (ℝ → Fin k)

The set of $k$-colorings of $\mathbb{R}$ that are multicolored on the translate $S + t$.

theorem LovaszLocalLemma.isClopen_eval_eq {k : ℕ} (x : ℝ) (i : Fin k) : IsClopen {c : ℝ → Fin k | c x = i}

The evaluation event $\{c : \mathbb{R} \to \text{Fin}\ k \mid c(x) = i\}$ is clopen in the product topology with discrete fibres.

theorem LovaszLocalLemma.isClosed_goodColorings {k : ℕ} (_hk : 0 < k) (S : Finset ℝ) (t : ℝ) : IsClosed (goodColorings k S t)

For $k \ge 1$, the set of colorings that are multicolored on $S + t$ is closed in the product topology.

theorem LovaszLocalLemma.lll_finite_coloring {m k : ℕ} (hk : 2 ≤ k) (hm : 1 ≤ m) (S : Finset ℝ) (hS : S.card = m) (hcond : Real.exp 1 * ↑(m * (m - 1) + 1) * ↑k * (1 - 1 / ↑k) ^ m ≤ 1) (T : Finset ℝ) : ∃ (c : ℝ → Fin k), ∀ t ∈ T, IsMulticolored k c (translate (↑S) t)

Finite-translate version (proved via the symmetric LLL): under the size condition $e \cdot (m(m-1) + 1) \cdot k \cdot (1 - 1/k)^m \le 1$, for any finite set of shifts $T$ there is a $k$-coloring of $\mathbb{R}$ that is multicolored on every translate $S + t$, $t \in T$.

theorem LovaszLocalLemma.erdos_lovasz_multicolor {m k : ℕ} (hk : 2 ≤ k) (hm : 1 ≤ m) (S : Finset ℝ) (hS : S.card = m) (hcond : Real.exp 1 * ↑(m * (m - 1) + 1) * ↑k * (1 - 1 / ↑k) ^ m ≤ 1) : ∃ (c : ℝ → Fin k), ∀ (t : ℝ), IsMulticolored k c (translate (↑S) t)

Erdős–Lovász multicolor theorem: under the same size condition, by compactness one obtains a single coloring of $\mathbb{R}$ that is multicolored on every translate $S + t$ for $t \in \mathbb{R}$.

def Beck.IsMonochromaticAP (c : ℤ → Bool) (k : ℕ) (a d : ℤ) : Prop

The arithmetic progression $a, a+d, \dots, a+(k-1)d$ is monochromatic under the $\{0,1\}$-coloring $c$ of $\mathbb{Z}$ if all of its $k$ terms have the same color as $a$.

theorem Beck.isOpen_monochromaticAP (k : ℕ) (a d : ℤ) : IsOpen {c : ℤ → Bool | IsMonochromaticAP c k a d}

The set of colorings under which a fixed AP $(a, d, k)$ is monochromatic is open in the product topology with discrete fibres.

theorem Beck.finite_consistency (ε : ℝ) (hε : 0 < ε) : ∃ (k₀ : ℕ), ∀ (n : ℕ) (constraints : Fin n → ℕ × ℤ × ℤ), (∀ (i : Fin n), k₀ ≤ (constraints i).1 ∧ 0 < (constraints i).2.2 ∧ ↑(constraints i).2.2 < 2 ^ ((1 - ε) * ↑(constraints i).1)) → ∃ (c : ℤ → Bool), ∀ (i : Fin n), ¬IsMonochromaticAP c (constraints i).1 (constraints i).2.1 (constraints i).2.2

Finite version of Beck's theorem on monochromatic APs: for any $\varepsilon > 0$ there is a threshold $k_0$ such that any finite list of AP constraints $(k, a, d)$ with $k \ge k_0$ and $0 < d < 2^{(1-\varepsilon) k}$ can be simultaneously broken by some $\{0,1\}$-coloring of $\mathbb{Z}$.

theorem Beck.beck_coloring_ap (ε : ℝ) (hε : 0 < ε) : ∃ (k₀ : ℕ) (c : ℤ → Bool), ∀ (k : ℕ), k₀ ≤ k → ∀ (a d : ℤ), 0 < d → ↑d < 2 ^ ((1 - ε) * ↑k) → ¬IsMonochromaticAP c k a d

Beck's theorem (via compactness): for any $\varepsilon > 0$ there exist a threshold $k_0$ and a $\{0,1\}$-coloring $c$ of $\mathbb{Z}$ such that no arithmetic progression of length $k \ge k_0$ with common difference $0 < d < 2^{(1-\varepsilon) k}$ is monochromatic under $c$.