English
A large family of vectors in R^n contains two distinct elements whose coordinate-wise remainders modulo b are close.
Русский
Большая семейство векторов в R^n содержит два различных элемента, координатные остатки которых по модулю b близки по каждому компоненту.
LaTeX
$$$\exists i_0 \neq i_1, \; \forall k, (abv (A_{i_1} k - A_{i_0} k) : \mathbb{R}) < abv(b) \cdot \varepsilon$$$
Lean4
/-- Any large enough family of vectors in `R^n` has a pair of elements
whose remainders are close together, pointwise. -/
theorem exists_approx_aux (n : ℕ) (h : abv.IsAdmissible) :
∀ {ε : ℝ} (_hε : 0 < ε) {b : R} (_hb : b ≠ 0) (A : Fin (h.card ε ^ n).succ → Fin n → R),
∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ k, (abv (A i₁ k % b - A i₀ k % b) : ℝ) < abv b • ε :=
by
haveI := Classical.decEq R
induction n with
| zero =>
intro ε _hε b _hb A
refine ⟨0, 1, ?_, ?_⟩
· simp
rintro ⟨i, ⟨⟩⟩
| succ n ih =>
intro ε hε b hb A
let M := h.card ε
obtain ⟨s, s_inj, hs⟩ :
∃ s : Fin (M ^ n).succ → Fin (M ^ n.succ).succ,
Function.Injective s ∧ ∀ i₀ i₁, (abv (A (s i₁) 0 % b - A (s i₀) 0 % b) : ℝ) < abv b • ε :=
by
-- We can partition the `A`s into `M` subsets where
-- the first components lie close together:
obtain ⟨t, ht⟩ :
∃ t : Fin (M ^ n.succ).succ → Fin M, ∀ i₀ i₁, t i₀ = t i₁ → (abv (A i₁ 0 % b - A i₀ 0 % b) : ℝ) < abv b • ε :=
h.exists_partition hε hb fun x ↦
A x
0
-- Since the `M` subsets contain more than `M * M^n` elements total,
-- there must be a subset that contains more than `M^n` elements.
obtain ⟨s, hs⟩ :=
Fintype.exists_lt_card_fiber_of_mul_lt_card (f := t)
(by simpa only [Fintype.card_fin, pow_succ'] using Nat.lt_succ_self (M ^ n.succ))
have : (M ^ n).succ ≤ (Finset.toList {x | t x = s}).length := by rwa [Finset.length_toList]
refine ⟨fun i ↦ (Finset.toList {x | t x = s})[i.castLE this], fun i j h ↦ ?_, fun i₀ i₁ ↦ ht _ _ ?_⟩
· simpa [(Finset.nodup_toList _).getElem_inj_iff, Fin.val_inj] using h
· have : ∀ (i : Fin (M ^ n).succ), t (Finset.toList {x | t x = s})[i.castLE this] = s := fun i ↦
(Finset.mem_filter.mp ((Finset.mem_toList (s := {x | t x = s})).mp (List.getElem_mem _))).2
simp_rw [this]
-- Since `s` is large enough, there are two elements of `A ∘ s`
-- where the second components lie close together.
obtain ⟨k₀, k₁, hk, h⟩ := ih hε hb fun x ↦ Fin.tail (A (s x))
refine ⟨s k₀, s k₁, fun h ↦ hk (s_inj h), fun i ↦ Fin.cases ?_ (fun i ↦ ?_) i⟩
· exact hs k₀ k₁
· exact h i
