term

Mathlib.NumberTheory.Harmonic.ZetaAsymp

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

← MathLib Explorer

English

The term is defined by the integral term(n,s) = ∫_n^{n+1} (x - n) / x^{s+1} dx.

Русский

Термин определяется как терм(n,s) = ∫_n^{n+1} (x - n) / x^{s+1} dx.

LaTeX

$$$\\\\operatorname{term}(n,s) = \\\\int_{n}^{n+1} \\\\frac{x - n}{x^{s+1}}\\\\,dx$$$

Lean4

/-- Auxiliary function used in studying zeta-function asymptotics. -/
noncomputable def term (n : ℕ) (s : ℝ) : ℝ :=
  ∫ x : ℝ in n..(n + 1), (x - n) / x ^ (s + 1)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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