partialSum — Mathlib

English

LiouvilleNumber.partialSum(m,k) is the sum of the first k+1 terms of Liouville's constant, i.e., sum_{i=0}^k 1/m^{i!}.

Русский

LiouvilleNumber.partialSum(m,k) — сумма первых k+1 членов константы Лиувилля: ∑_{i=0}^k 1/m^{i!}.

LaTeX

$$$\\mathrm{partialSum}(m,k)=\\sum_{i=0}^{k} m^{-i!}$$$

Lean4

/-- `LiouvilleNumber.partialSum` is the sum of the first `k + 1` terms of Liouville's constant,
i.e.
$$
\sum_{i=0}^k\frac{1}{m^{i!}}.
$$
-/
def partialSum (m : ℝ) (k : ℕ) : ℝ :=
  ∑ i ∈ range (k + 1), 1 / m ^ i !

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