Approximation by grid vectors

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

Truncating each coordinate toward zero gives a vector on N⁻¹ • ℤ ^ d. The error in each coordinate is at most 1 / N, and no coordinate increases in absolute value. In particular, the approximation does not increase the Euclidean norm.

theorem Komlos.exists_int_approx (x : ℝ) {N : ℕ} (hN : 0 < N) : ∃ (m : ℤ), |↑m / ↑N| ≤ |x| ∧ |x - ↑m / ↑N| ≤ 1 / ↑N

Truncation toward zero on the grid N⁻¹ • ℤ.

theorem Komlos.exists_grid_approx {d n : ℕ} (v : Fin n → Fin d → ℝ) {η : ℝ} (hη : 0 < η) : ∃ (N : ℕ) (g : Fin n → Fin d → ℤ), 0 < N ∧ (∀ (i : Fin n) (k : Fin d), |↑(g i k) / ↑N| ≤ |v i k|) ∧ ∀ (i : Fin n) (k : Fin d), |v i k - ↑(g i k) / ↑N| ≤ η

Approximate finitely many vectors on a common grid within η in each coordinate, without increasing any coordinate in absolute value.