term_sum

Mathlib.NumberTheory.Harmonic.ZetaAsymp

URI: https://scilib.ai/kg/mathlib#ZetaAsymptotics.term_sum

English

The finite sum of terms is defined by term_sum(s,N) = sum_{n=0}^{N-1} term(n+1,s).

Русский

Конечная сумма терминов определяется как term_sum(s,N) = \\\\sum_{n=0}^{N-1} term(n+1,s).

LaTeX

$$$\\\\operatorname{term\\_sum}(s,N) = \\\\sum_{n=0}^{N-1} \\\\operatorname{term}(n+1,s)$$$

Lean4

/-- Sum of finitely many `term`s. -/
noncomputable def term_sum (s : ℝ) (N : ℕ) : ℝ :=
  ∑ n ∈ Finset.range N, term (n + 1) s

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru