tendsto_harmonic_sub_log_add_one

Mathlib.NumberTheory.Harmonic.EulerMascheroni

URI: https://scilib.ai/kg/mathlib#Real.tendsto_harmonic_sub_log_add_one

← MathLib Explorer

English

The sequence a_n = H_n − log(n+1) converges to γ as n → ∞.

Русский

Последовательность a_n = H_n − log(n+1) сходится к γ при стремлении n к бесконечности.

LaTeX

$$\lim_{n\to\infty} \left(H_n - \log(n+1)\right) = \gamma$$

Lean4

theorem tendsto_harmonic_sub_log_add_one :
    Tendsto (fun n : ℕ ↦ harmonic n - log (n + 1)) atTop (𝓝 eulerMascheroniConstant) :=
  tendsto_eulerMascheroniSeq

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

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

Разделы

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

Аффилиация

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