The Komlós bound on a grid

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

For vectors on N⁻¹ • ℤ ^ d, the distribution from Lemma 1.5 satisfies the hypotheses of Lemma 1.4 after scaling the vectors by 1 / 6. The resulting signed sum has supremum norm at most 36.

theorem Komlos.discrepancy_le_of_grid {d n N : ℕ} (hN : 0 < N) (g : Fin n → Fin d → ℤ) (hg : ∀ (i : Fin n), ∑ k : Fin d, (↑(g i k) / ↑N) ^ 2 ≤ 1) : discrepancy (Matrix.of fun (k : Fin d) (i : Fin n) => ↑(g i k) / ↑N) ≤ 36

The Komlós conjecture for grid vectors: a matrix whose columns lie on the grid N⁻¹ • ℤ ^ d and have Euclidean norm at most 1 has discrepancy at most 36.