theorem Discrepancy.komlos_conjecture : ∃ (K : ℝ), 0 < K ∧ ∀ (n m : ℕ) (v : Fin m → EuclideanSpace ℝ (Fin n)), (∀ (i : Fin m), ‖v i‖ ≤ 1) → ∃ (ε : Fin m → ℝ), (∀ (i : Fin m), ε i = 1 ∨ ε i = -1) ∧ ∀ (j : Fin n), |∑ i : Fin m, ε i * (v i).ofLp j| ≤ K

Komlós conjecture (Conjecture 5.1.5). There exists an absolute constant $K > 0$ such that for any vectors $v_1, \dots, v_m \in \mathbb{R}^n$ with $\|v_i\| \leq 1$, one can choose signs $\varepsilon_i \in \{\pm 1\}$ so that $\left\|\sum_i \varepsilon_i v_i\right\|_\infty \leq K$.