summable_ofDigitsTerm — Mathlib

English

The sequence of terms ofDigitsTerm is summable (the series converges).

Русский

Последовательность ofDigitsTerm суммируема, то есть ряд сходится.

LaTeX

$$$\operatorname{Summable}\bigl(\mathrm{Real.ofDigitsTerm}(\text{digits})\bigr)$$$

Lean4

theorem summable_ofDigitsTerm {b : ℕ} {digits : ℕ → Fin b} : Summable (ofDigitsTerm digits) :=
  by
  refine Summable.of_nonneg_of_le (fun _ ↦ ofDigitsTerm_nonneg) (fun _ ↦ ofDigitsTerm_le) ?_
  obtain rfl | hb := (Nat.one_le_of_lt (b_pos digits)).eq_or_lt
  · simpa using summable_zero
  simp_rw [pow_succ', mul_inv, ← inv_pow, ← mul_assoc]
  refine Summable.mul_left _ (summable_geometric_of_lt_one (by positivity) ?_)
  simp [inv_lt_one_iff₀, hb]

Похожие утверждения