English
Under suitable base and range conditions, the infinite series of ofDigitsTerm(digits x b) has sum x.
Русский
При подходящем основании и условиях х определено, что сумма ряда ofDigitsTerm(digits x b) равна x.
LaTeX
$$$\forall x \in [0,1), \; b > 1: \mathrm{HasSum}(\mathrm{Real.ofDigitsTerm}(\mathrm{digits}(x,b)), x)$$$
Lean4
theorem hasSum_ofDigitsTerm_digits (x : ℝ) {b : ℕ} [NeZero b] (hb : 1 < b) (hx : x ∈ Set.Ico 0 1) :
HasSum (ofDigitsTerm (digits x b)) x :=
by
rw [hasSum_iff_tendsto_nat_of_summable_norm (by exact summable_ofDigitsTerm.abs)]
refine
tendsto_of_tendsto_of_tendsto_of_le_of_le ?_ tendsto_const_nhds (le_sum_ofDigitsTerm_digits hb hx)
(sum_ofDigitsTerm_digits_le hx)
convert tendsto_const_nhds.sub (tendsto_pow_atTop_nhds_zero_of_abs_lt_one _)
· simp
· simp [abs_of_nonneg, inv_lt_one_iff₀, hb]
