English
For any finite family indexed by ι, there exist distinct indices i0,i1 such that the coordinate-wise remainders of A(i1) and A(i0) are close modulo b.
Русский
Для любой конечной семейства индексы i0,i1 существуют такие, что координатные остатки A(i1) и A(i0) по модулю b близки.
LaTeX
$$$\exists i_0 \neq i_1, \; \forall k, (abv (A(i_1) k \% b - A(i_0) k \% b) : \mathbb{R}) < abv(b) \cdot \varepsilon$$$
Lean4
/-- Any large enough family of vectors in `R^ι` has a pair of elements
whose remainders are close together, pointwise. -/
theorem exists_approx {ι : Type*} [Fintype ι] {ε : ℝ} (hε : 0 < ε) {b : R} (hb : b ≠ 0) (h : abv.IsAdmissible)
(A : Fin (h.card ε ^ Fintype.card ι).succ → ι → R) :
∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ k, (abv (A i₁ k % b - A i₀ k % b) : ℝ) < abv b • ε :=
by
let e := Fintype.equivFin ι
obtain ⟨i₀, i₁, ne, h⟩ := h.exists_approx_aux (Fintype.card ι) hε hb fun x y ↦ A x (e.symm y)
refine ⟨i₀, i₁, ne, fun k ↦ ?_⟩
convert h (e k) <;> simp only [e.symm_apply_apply]
