partialSum_succ — Mathlib

English

Let m be a real number and n a natural number. Then the (n+1)-th partial sum of the Liouville series with base m equals the nth partial sum plus 1 divided by m to the power (n+1)!, i.e. S_m(n+1) = S_m(n) + 1 / m^{(n+1)!}.

Русский

Пусть m — вещественное число, n — натуральное. Тогда (n+1)-я частичная сумма ряда Лиувиля с основанием m равна n-ой частичной сумме плюс 1 делить на m в степени (n+1)!, т.е. S_m(n+1) = S_m(n) + 1 / m^{(n+1)!}.

LaTeX

$$$ \partialSum m (n + 1) = \partialSum m n + \frac{1}{m^{(n + 1)!}} $$$

Lean4

theorem partialSum_succ (m : ℝ) (n : ℕ) : partialSum m (n + 1) = partialSum m n + 1 / m ^ (n + 1)! :=
  sum_range_succ _ _

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