English
For a Real x, base b with NeZero b, and hx ∈ [0,1), we have: b^n ∑_{i=0}^{n-1} ofDigitsTerm (digits x b) i = ⌊ b^n x ⌋_+ for all n.
Русский
Для действительного x и основания b с ненулевостью, при hx ∈ [0,1) выполняется: для всех n выполняется указанная равенство с floor.
LaTeX
$$$\forall {x : \mathbb{R}} {b : \mathbb{N}} [\mathrm{NeZero}~b] \; (x \in [0,1)) \; (n : \mathbb{N}) : b^n \sum_{i=0}^{n-1} \mathrm{Real.ofDigitsTerm}(\mathrm{digits}(x,b)) i = \lfloor b^n x \rfloor_{+}$$$
Lean4
theorem ofDigits_digits_sum_eq {x : ℝ} {b : ℕ} [NeZero b] (hx : x ∈ Set.Ico 0 1) (n : ℕ) :
b ^ n * ∑ i ∈ Finset.range n, ofDigitsTerm (digits x b) i = ⌊b ^ n * x⌋₊ :=
by
have := NeZero.ne b
induction n with
| zero => simp [Nat.floor_eq_zero.mpr hx.right]
| succ n
ih =>
rw [Finset.sum_range_succ, mul_add, pow_succ', mul_assoc, ih, ofDigitsTerm, digits, ← pow_succ', mul_left_comm,
mul_inv_cancel₀ (by positivity), mul_one, mul_comm x, pow_succ', mul_assoc]
set y := (b : ℝ) ^ n * x
norm_cast
rw [← Nat.cast_mul_floor_div_cancel (a := y) (show b ≠ 0 by cutsat), Fin.val_ofNat, Nat.div_add_mod]
