English
For x ∈ [0,1) and any n, b^n ∑_{i=0}^{n-1} ofDigitsTerm (digits x b) i = ⌊ b^n x ⌋_+.
Русский
Для x ∈ [0,1) и любого n выполняется: b^n · ∑_{i=0}^{n-1} ofDigitsTerm (digits x b) i = ⌊ b^n x ⌋_+.
LaTeX
$$$\forall {x : \mathbb{R}} {b : \mathbb{N}} [\mathrm{NeZero}~b] (hx : x \in [0,1)) (n : \mathbb{N}), b^n \cdot \sum_{i=0}^{n-1} \mathrm{Real.ofDigitsTerm}(\mathrm{digits}(x,b)) i = \lfloor b^n x \rfloor_{+}$$$
Lean4
theorem ofDigits_eq_sum_add_ofDigits {b : ℕ} (a : ℕ → Fin b) (n : ℕ) :
ofDigits a = (∑ i ∈ Finset.range n, ofDigitsTerm a i) + ((b : ℝ) ^ n)⁻¹ * ofDigits (fun i ↦ a (i + n)) :=
by
simp only [ofDigits]
rw [← Summable.sum_add_tsum_nat_add n summable_ofDigitsTerm, ← Summable.tsum_mul_left _ summable_ofDigitsTerm]
congr
ext i
simp only [ofDigitsTerm]
ring
