partialSum_add_remainder — Mathlib

English

Let m > 1 and k be a natural number. Then liouvilleNumber m equals the sum of the first k partial sums plus the remainder: partialSum m k + remainder m k = liouvilleNumber m.

Русский

Пусть m > 1 и k ∈ ℕ. Тогда число Лиувиля с основанием m равно сумме первых k слагаемых и остатка: partialSum m k + remainder m k = liouvilleNumber m.

LaTeX

$$$ (1 < m) \implies (\partialSum m k + \mathrm{remainder} m k = \liouvilleNumber m) $$$

Lean4

/-- Split the sum defining a Liouville number into the first `k` terms and the rest. -/
theorem partialSum_add_remainder {m : ℝ} (hm : 1 < m) (k : ℕ) : partialSum m k + remainder m k = liouvilleNumber m :=
  (LiouvilleNumber.summable hm).sum_add_tsum_nat_add _

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