English
If x and y are digit-sequences that agree up to index n, then the difference between their digit-sum representations is small: |ofDigits x − ofDigits y| ≤ (b^n)⁻¹.
Русский
Если последовательности цифр x и y совпадают на всех позициях i < n, то разность их представлений ограничена: |ofDigits x − ofDigits y| ≤ (b^n)⁻¹.
LaTeX
$$$\forall {b} {x y : \mathbb{N} \to \mathrm{Fin} b} {n} (\forall i < n, x i = y i) \Rightarrow |\mathrm{ofDigits}(x) - \mathrm{ofDigits}(y)| \le (b^n)^{-1}$$$
Lean4
theorem abs_ofDigits_sub_ofDigits_le {b : ℕ} {x y : ℕ → Fin b} {n : ℕ} (hxy : ∀ i < n, x i = y i) :
|ofDigits x - ofDigits y| ≤ ((b : ℝ) ^ n)⁻¹ :=
by
rw [ofDigits_eq_sum_add_ofDigits x n, ofDigits_eq_sum_add_ofDigits y n]
have : ∑ i ∈ Finset.range n, ofDigitsTerm x i = ∑ i ∈ Finset.range n, ofDigitsTerm y i :=
Finset.sum_congr rfl fun i hi ↦ by simp [ofDigitsTerm, hxy i (Finset.mem_range.mp hi)]
rw [this, add_sub_add_left_eq_sub, ← mul_sub, abs_mul, abs_of_nonneg (by positivity)]
apply mul_le_of_le_one_right (by positivity)
convert abs_sub_le_of_le_of_le (ofDigits_nonneg _) (ofDigits_le_one _) (ofDigits_nonneg _) (ofDigits_le_one _)
simp
