English
There exists a partition of a finite family of integers modulo a nonzero integer b into blocks so that within each block the residues modulo b are close to each other, within ε·|b|.
Русский
Существует разбиение конечной семейства целых чисел по модулю на блоки так, что внутри блока остатки по модулю b близки друг к другу в пределах ε·|b|.
LaTeX
$$$\exists t:\, Fin\ n \to Fin\lceil 1/\varepsilon\rceil_+ ,\; \forall i_0,i_1,\; t(i_0)=t(i_1) \Rightarrow \left|A(i_1) \bmod b - A(i_0) \bmod b\right| < |b|\varepsilon$$$
Lean4
/-- We can partition a finite family into `partition_card ε` sets, such that the remainders
in each set are close together. -/
theorem exists_partition_int (n : ℕ) {ε : ℝ} (hε : 0 < ε) {b : ℤ} (hb : b ≠ 0) (A : Fin n → ℤ) :
∃ t : Fin n → Fin ⌈1 / ε⌉₊, ∀ i₀ i₁, t i₀ = t i₁ → ↑(abs (A i₁ % b - A i₀ % b)) < abs b • ε :=
by
have hb' : (0 : ℝ) < ↑(abs b) := Int.cast_pos.mpr (abs_pos.mpr hb)
have hbε : 0 < abs b • ε := by
rw [Algebra.smul_def]
exact mul_pos hb' hε
have hfloor : ∀ i, 0 ≤ floor ((A i % b : ℤ) / abs b • ε : ℝ) := fun _ ↦
floor_nonneg.mpr (div_nonneg (cast_nonneg.mpr (emod_nonneg _ hb)) hbε.le)
refine ⟨fun i ↦ ⟨natAbs (floor ((A i % b : ℤ) / abs b • ε : ℝ)), ?_⟩, ?_⟩
· rw [← ofNat_lt, natAbs_of_nonneg (hfloor i), floor_lt, Algebra.smul_def, eq_intCast, ← div_div]
apply lt_of_lt_of_le _ (Nat.le_ceil _)
gcongr
rw [div_lt_one hb', cast_lt]
exact Int.emod_lt_abs _ hb
intro i₀ i₁ hi
have hi : (⌊↑(A i₀ % b) / abs b • ε⌋.natAbs : ℤ) = ⌊↑(A i₁ % b) / abs b • ε⌋.natAbs :=
congr_arg ((↑) : ℕ → ℤ) (Fin.mk_eq_mk.mp hi)
rw [natAbs_of_nonneg (hfloor i₀), natAbs_of_nonneg (hfloor i₁)] at hi
have hi := abs_sub_lt_one_of_floor_eq_floor hi
rw [abs_sub_comm, ← sub_div, abs_div, abs_of_nonneg hbε.le, div_lt_iff₀ hbε, one_mul] at hi
rwa [Int.cast_abs, Int.cast_sub]
