Partial colouring via Kleitman's diameter theorem

Proved

Komlos.partial_coloring_via_kleitman

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

combinatoricsdiscrepancykleitmanpartial-coloringspencer

Let $A$ be an $n \times n$ matrix with entries in $\{0,1\}$ , let $T$ be a nonempty set of columns with $r = |T|$ , let $s$ be a natural number with $2s < r$ , and let $\nu \ge 0$ satisfy the budget inequality

n \cdot 2 e^{-\nu^2/2} < 1 - \exp\left(-r\left(\ln 2 - H(s/r)\right)\right),

where $H(p) = -p \ln p - (1-p)\ln(1-p)$ is the binary entropy function (in nats). Then there is a partial colouring $\chi \in \{-1,0,+1\}^n$ , vanishing outside $T$ , which colours more than $2s$ of the columns in $T$ ,

\#\{j \in T : \chi_j \neq 0\} > 2s,

and keeps every row balanced to within $\nu\sqrt{r}$ :

\left|\sum_{j\in T}A_{ij}\chi_j\right| \le \nu\sqrt{r} \qquad \text{for every } i.

This is a reduction of Spencer's partial-colouring step (the entropy method of J. Spencer, Six standard deviations suffice, 1985) to Kleitman's diameter theorem (kleitman_diameter, submitted separately): a union bound over sub-Gaussian row-sum tail bounds gives a 'good' set of colourings of size at least $2^r(1 - n\cdot 2e^{-\nu^2/2})$ ; the classical entropy bound on binomial sums (choose_sum_le_exp_mul_binEntropy) shows this exceeds the size of a Hamming ball of radius $s$ exactly when the budget inequality holds; Kleitman's theorem then produces two colourings in the good set at Hamming distance greater than $2s$ , and their difference (divided by 2) is the desired partial colouring, since two row sums each within $\nu\sqrt{r}$ average to a row sum within $\nu\sqrt{r}$ .

Formalization Note. This is deliberately not a literal formalization of the captain-curated Komlos.spencer_partial_coloring (whose budget hypothesis is stated with different, sharper constants tuned to Spencer's own numerical schedule) — it is a faithful, independently-derivable reduction with the same conclusion shape and the same combinatorial mechanism, isolating Kleitman's theorem as the single remaining unproved ingredient. The conclusion is phrased with the natural number $s$ (colouring more than $2s$ of $T$ ) rather than a real fraction $\theta$ , matching Kleitman's theorem's own output exactly.

Preamble

import Mathlib
open Finset MeasureTheory ProbabilityTheory Real
open scoped Classical

Formal statement

namespace Komlos

theorem partial_coloring_via_kleitman
    {n : ℕ} (A : Fin n → Fin n → ℝ) (T : Finset (Fin n))
    (h01 : ∀ i j, A i j = 0 ∨ A i j = 1) (hT : 0 < T.card)
    (s : ℕ) (hs : 2 * s < T.card) (ν : ℝ) (hν : 0 ≤ ν)
    (hbudget : (n : ℝ) * 2 * Real.exp (-ν ^ 2 / 2)
        < 1 - Real.exp (-(T.card : ℝ) * (Real.log 2 - Real.binEntropy ((s : ℝ) / T.card)))) :
    ∃ χ : Fin n → ℝ,
      (∀ j, χ j = 1 ∨ χ j = -1 ∨ χ j = 0) ∧
      (∀ j, j ∉ T → χ j = 0) ∧
      2 * s < (T.filter (fun j => χ j ≠ 0)).card ∧
      (∀ i, |∑ j ∈ T, A i j * χ j| ≤ ν * Real.sqrt T.card) := by sorry

end Komlos

Source

Original reduction, following the method of J. Spencer, Six standard deviations suffice, Trans. Amer. Math. Soc. 289 (1985) 679-706, Section 2 (digitization + entropy pigeonhole + Kleitman's diameter theorem), but with the digitization step replaced by a direct union bound over sub-Gaussian row-sum tail bounds (Hoeffding's inequality via HasSubgaussianMGF, as used for Komlos.spencer_random_finish) and independently-derived budget constants, rather than Spencer's original numerical schedule. Kleitman's theorem itself: D. J. Kleitman, Families of non-disjoint subsets, J. Combinatorial Theory 1 (1966), 153-155.

View graph