Staged partial colouring within the six-deviation budget

Open

Komlos.spencer_staged_partial_coloring_budget

by Yuning · Sep 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

combinatoricsdiscrepancypartial-coloringspencer

Assume the stated Spencer partial-colouring step for every nonempty active set. Then, for every $n\times n$ $0/1$ matrix $A$ , there are a residual set $T$ and a partial sign vector $\psi$ such that $\psi$ vanishes on $T$ , takes values in $\{\pm1\}$ outside $T$ , and for every row $i$ ,

\left|\sum_j A_{ij}\psi_j\right|+\sqrt{2|T|\log(4n)}\le 6\sqrt n.

The first term is the discrepancy accumulated while iterating the partial-colouring step; the second is exactly the budget reserved for a final union-bound colouring of the residual set. This theorem isolates the recursive schedule, parameter choices, termination, and sharp numerical summation without assuming the residual-colouring theorem.

Preamble

import Definitions.Def_Komlos_model
open Finset

Formal statement

namespace Komlos

/-- Iterating the partial-colouring step leaves a residual set whose random
completion cost, added to the accumulated discrepancy, fits the Spencer budget. -/
theorem spencer_staged_partial_coloring_budget
    (pcl : ∀ (n : ℕ) (A : Fin n → Fin n → ℝ), (∀ i j, A i j = 0 ∨ A i j = 1) →
      ∀ (T : Finset (Fin n)), 0 < T.card → ∀ θ ν : ℝ, 0 < θ → θ ≤ 1 / 2 → 2 ≤ ν →
        (n : ℝ) * (2 * Real.exp (-(ν ^ 2) / 2) * (3 * ν ^ 2 / 4 + 2))
            ≤ (2 / 3) * θ ^ 2 * (T.card : ℝ) →
        ∃ χ : Fin n → ℝ,
          (∀ j, χ j = 1 ∨ χ j = -1 ∨ χ j = 0) ∧
          (∀ j, j ∉ T → χ j = 0) ∧
          (1 - θ) * (T.card : ℝ) ≤ ((T.filter (fun j => χ j ≠ 0)).card : ℝ) ∧
          (∀ i, |∑ j ∈ T, A i j * χ j| ≤ ν * Real.sqrt (T.card : ℝ)))
    (n : ℕ) (A : Fin n → Fin n → ℝ) (h01 : ∀ i j, A i j = 0 ∨ A i j = 1) :
    ∃ (T : Finset (Fin n)) (ψ : Fin n → ℝ),
      (∀ j, j ∈ T → ψ j = 0) ∧
      (∀ j, j ∉ T → ψ j = 1 ∨ ψ j = -1) ∧
      ∀ i,
        |∑ j, A i j * ψ j| +
            Real.sqrt (2 * (T.card : ℝ) * Real.log (4 * n))
          ≤ 6 * Real.sqrt n := by
  sorry

end Komlos

Source

J. Spencer, Six standard deviations suffice, Trans. Amer. Math. Soc. 289 (1985), Theorem 1 and Section 2 partial-colouring iteration; https://doi.org/10.1090/S0002-9947-1985-0784009-0. Reduction child for Prove2Me theorem Komlos.spencer_recursion.

View graph