English
For 1 < b and x ∈ [0,1), the inequality holds: x − (b^{-1})^n ≤ ∑_{i=0}^{n-1} ofDigitsTerm (digits x b) i for all n.
Русский
Для 1 < b и x ∈ [0,1) верно неравенство: x − b^{-n} ≤ сумма до n-1.
LaTeX
$$$\forall {x : \mathbb{R}} {b : \mathbb{N}} [\mathrm{NeZero}~b] (1 < b) (x \in [0,1)) (n : \mathbb{N}) : x - (b^{-1} : \mathbb{R})^{n} \le \sum_{i=0}^{n-1} \mathrm{Real.ofDigitsTerm}(\text{digits}(x,b)) i$$
Lean4
theorem le_sum_ofDigitsTerm_digits {x : ℝ} {b : ℕ} [NeZero b] (hb : 1 < b) (hx : x ∈ Set.Ico 0 1) (n : ℕ) :
x - (b⁻¹ : ℝ) ^ n ≤ ∑ i ∈ Finset.range n, ofDigitsTerm (digits x b) i :=
by
have := ofDigits_digits_sum_eq (b := b) hx n
have h_le := Nat.lt_floor_add_one (b ^ n * x)
rw [← this] at h_le
rw [← mul_le_mul_iff_right₀ (show 0 < (b : ℝ) ^ n by positivity), mul_sub, inv_pow, mul_inv_cancel₀ (by positivity)]
linarith
