Spencer's discrepancy theorem, $O(\\sqrt n)$ form

Proved

spencer_discrepancy_sqrt_n_bound

by xbgxjack · Sep 10, 2026 · Mathlib 0df444a (Lean v4.33.1)

combinatoricsdiscrepancy-theoryentropy-methodprobabilistic-method

This is the asymptotic (constant-suppressed) form of Spencer's "six standard deviations suffice" discrepancy theorem, proved via the entropy method exactly as presented in Rothvöß's course notes (Theorem 7 there), rather than with Spencer's original sharp constant $6$ .

Let $n$ be a positive integer and let $A$ be an $n\\times n$ matrix with entries in $\\{0,1\\}$ , thought of as the incidence matrix of $n$ sets over an $n$ -element ground set. The claim is that there is a single universal constant $C$ (not depending on $n$ or $A$ ) and a sign vector $\\varepsilon\\in\\{-1,+1\\}^n$ such that every row sum is controlled:

\\exists\\, C\\in\\mathbb R,\\ \\forall n\\ge 1,\\ \\forall A\\in\\{0,1\\}^{n\\times n},\\ \\exists\\,\\varepsilon\\in\\{-1,1\\}^n,\\ \\forall i,\\ \\Bigl|\\sum_{j=1}^n A_{ij}\\,\\varepsilon_j\\Bigr|\\le C\\sqrt n.

A uniformly random $\\pm1$ coloring only achieves discrepancy $\\Theta(\\sqrt{n\\log n})$ with high probability; the content of the theorem is that the $\\log n$ factor can be removed entirely, for every $n\\times n$ $0/1$ matrix, at the cost of an unspecified (but $n$ -independent) multiplicative constant. This is the qualitative heart of Spencer's discrepancy theorem and the standard entry point for applications that only need an $O(\\sqrt n)$ bound rather than the literal constant $6$ .

Formalization Note. The sign vector is represented as a function $\\varepsilon:\\mathrm{Fin}\\,n\\to\\mathbb R$ constrained pointwise to $\\{-1,1\\}$ , matching the usual $\\{\\pm1\\}$ -coloring convention; the existential quantifier on $C$ is placed outermost so that the SAME constant works uniformly across every $n$ and every matrix $A$ , which is what makes this an $O(\\sqrt n)$ statement rather than a per-instance bound.

Preamble

import Mathlib
open Finset

Formal statement

theorem spencer_discrepancy_sqrt_n_bound :
    ∃ C : ℝ, ∀ (n : ℕ), 0 < n → ∀ (A : Fin n → Fin n → ℝ),
      (∀ i j, A i j = 0 ∨ A i j = 1) →
      ∃ ε : Fin n → ℝ, (∀ j, ε j = 1 ∨ ε j = -1) ∧
        ∀ i, |∑ j, A i j * ε j| ≤ C * Real.sqrt (n : ℝ) := by sorry

Source

J. Spencer, "Six standard deviations suffice", Trans. Amer. Math. Soc. 289 (1985), 679–706, Theorem 1 (qualitative O(sqrt n) form, not the sharp constant 6), https://doi.org/10.1090/S0002-9947-1985-0784009-0; proved here via the entropy / partial-coloring method as expounded in T. Rothvoß, "Discrepancy theory, or: how much balance is possible?", MIT lecture notes, Theorem 7 and Section 4 (Lemma 8, Lemma 9), https://math.mit.edu/classes/18.095/lect6/notes.pdf

Human review

Endorsed by Shuze Chen · Sep 11, 2026
Endorsed by xbgxjack · Sep 11, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Spencer's discrepancy theorem, O(sqrtn)O(\\sqrt n)O(sqrtn) form

Spencer's discrepancy theorem, $O(\\sqrt n)$ form