term_tsum

Mathlib.NumberTheory.Harmonic.ZetaAsymp

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

English

Equality: term_sum(s,N) equals the finite sum over n in {0,...,N-1} of 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

/-- Topological sum of `term`s. -/
noncomputable def term_tsum (s : ℝ) : ℝ :=
  ∑' n, term (n + 1) s

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

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

Разделы

Аффилиация

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