English
For x ∈ [0,1) and any n, the partial sum of the ofDigitsTerm terms is at most x: ∑_{i=0}^{n-1} ofDigitsTerm (digits x b) i ≤ x.
Русский
Для x ∈ [0,1) и любого n частичная сумма членов ofDigitsTerm не превосходит x.
LaTeX
$$$\forall {x : \mathbb{R}} {b : \mathbb{N}} [\mathrm{NeZero}~b] (x \in [0,1)) (n : \mathbb{N}) : \sum_{i=0}^{n-1} \mathrm{Real.ofDigitsTerm}(\text{digits}(x,b)) i \le x$$$
Lean4
theorem sum_ofDigitsTerm_digits_le {x : ℝ} {b : ℕ} [NeZero b] (hx : x ∈ Set.Ico 0 1) (n : ℕ) :
∑ i ∈ Finset.range n, ofDigitsTerm (digits x b) i ≤ x :=
by
have := ofDigits_digits_sum_eq (b := b) hx n
have h_le := Nat.floor_le (a := b ^ n * x) (by have := hx.left; positivity)
have hb := NeZero.ne b
rw [← this, mul_le_mul_iff_of_pos_left (by positivity)] at h_le
exact h_le
