theorem Discrepancy.spencer_six_std_dev (n : ℕ) (F : Fin n → Finset (Fin n)) : ∃ (f : Fin n → ℤ), (∀ (i : Fin n), f i = 1 ∨ f i = -1) ∧ ∀ (j : Fin n), |↑(∑ i ∈ F j, f i)| ≤ 6 * √↑n

Theorem 5.1.1 (Spencer 1985, "six standard deviations suffice"). Given any system of $n$ subsets of an $n$-element ground set, there exists a $\pm 1$ colouring $f$ such that every set has discrepancy at most $6\sqrt n$.

theorem Discrepancy.spencer_six_std_dev_general : ∃ C > 0, ∀ (n m : ℕ), m ≥ n → n ≥ 1 → ∀ (F : Fin m → Finset (Fin n)), ∃ (f : Fin n → ℤ), (∀ (i : Fin n), f i = 1 ∨ f i = -1) ∧ ∀ (j : Fin m), |↑(∑ i ∈ F j, f i)| ≤ C * √(↑n * Real.log (2 * ↑m / ↑n))

Theorem 5.1.3 (general Spencer bound). For any system of $m \ge n$ subsets of an $n$-element ground set there is a $\pm 1$ colouring achieving discrepancy $O(\sqrt{n \log(2m/n)})$.

noncomputable def Discrepancy.interiorIndices {m : ℕ} (a : Fin m → ℝ) : Finset (Fin m)

Indices at which a vector $a \in [-1,1]^m$ is in the open interior, i.e. neither $1$ nor $-1$. The discrepancy argument rounds these to a $\pm 1$ vector.

def Discrepancy.IsFeasible {n m : ℕ} (v : Fin m → Fin n → ℝ) (a : Fin m → ℝ) : Prop

Feasibility predicate for the rounding step: a vector $a \in [-1,1]^m$ is feasible with respect to vectors $v_1, \dots, v_m \in \mathbb{R}^n$ if $\sum_i a_i v_i = 0$.

theorem Discrepancy.feasible_improve {n m : ℕ} (v : Fin m → Fin n → ℝ) (a : Fin m → ℝ) (hfeas : IsFeasible v a) (hcard : n < (interiorIndices a).card) : ∃ (a' : Fin m → ℝ), IsFeasible v a' ∧ (interiorIndices a').card < (interiorIndices a).card

Pivoting step. Given a feasible $a$ with more than $n$ interior coordinates, there is another feasible $a'$ with strictly fewer interior coordinates, obtained by moving along a linear dependency among the $v_i$'s on the interior set.

theorem Discrepancy.discrepancy_technical_lemma (n m : ℕ) (v : Fin m → Fin n → ℝ) : ∃ (a : Fin m → ℝ), (∀ (i : Fin m), a i ∈ Set.Icc (-1) 1) ∧ (interiorIndices a).card ≤ n ∧ ∑ i : Fin m, a i • v i = 0

Iterating the pivoting step yields the technical rounding lemma underlying Spencer's theorem: starting from $a = 0$ one can find a feasible $a \in [-1,1]^m$ with at most $n$ coordinates in the open interior.