The Komlós bound

Adapted for Lean Pool by changing module paths and selecting explicit imports.

A real matrix whose columns have Euclidean norm at most 1 has discrepancy at most 36. The file proves this for arbitrary finite row and column types, then gives the scaled bound and the equivalent statements for vectors and colourings.

The proof uses Komlos.discrepancy_le_of_grid. Given η > 0, approximate each matrix entry within η / (n + 1), where n is the number of columns. A colouring for the approximation has discrepancy at most 36 + η for the original matrix. Letting η tend to zero gives the bound.

theorem Komlos.discrepancy_le_of_forall_sum_sq_le_one_fin {d n : ℕ} (A : Matrix (Fin d) (Fin n) ℝ) (hA : ∀ (j : Fin n), ∑ i : Fin d, A i j ^ 2 ≤ 1) : discrepancy A ≤ 36

Theorem 1.2 for matrices with rows indexed by Fin d and columns indexed by Fin n.

theorem Komlos.discrepancy_le_of_forall_sum_sq_le_one {m : Type u_1} {n : Type u_2} [Fintype m] [Fintype n] (A : Matrix m n ℝ) (hA : ∀ (j : n), ∑ i : m, A i j ^ 2 ≤ 1) : discrepancy A ≤ 36

Theorem 1.2 (Komlós conjecture, with constant 36): a real matrix whose columns have Euclidean norm at most 1 has discrepancy at most 36.

theorem Komlos.discrepancy_le_of_forall_sum_sq_le {m : Type u_1} {n : Type u_2} [Fintype m] [Fintype n] (A : Matrix m n ℝ) {C : ℝ} (hC : 0 ≤ C) (hA : ∀ (j : n), ∑ i : m, A i j ^ 2 ≤ C ^ 2) : discrepancy A ≤ 36 * C

Theorem 1.2, scaled: a real matrix whose columns have Euclidean norm at most C has discrepancy at most 36 * C.

theorem Komlos.discrepancy_le_of_forall_norm_le_one {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] (v : ι → EuclideanSpace ℝ κ) (hv : ∀ (i : ι), ‖v i‖ ≤ 1) : discrepancy (Matrix.of fun (k : κ) (i : ι) => (v i).ofLp k) ≤ 36

Theorem 1.2, Euclidean form: if v i ∈ ℝ ^ κ have Euclidean norm at most 1, then the matrix with columns v i has discrepancy at most 36.

theorem Komlos.exists_isColouring_forall_abs_sum_apply_le {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] (v : ι → EuclideanSpace ℝ κ) (hv : ∀ (i : ι), ‖v i‖ ≤ 1) : ∃ (ε : ι → ℝ), IsColouring ε ∧ ∀ (k : κ), |(∑ i : ι, ε i • v i).ofLp k| ≤ 36

Theorem 1.2, colouring form: vectors of Euclidean norm at most 1 admit a colouring whose signed sum has every coordinate bounded by 36.