tendsto_eulerMascheroniSeq' — Mathlib

English

The modified Euler–Mascheroni sequence eulerMascheroniSeq' converges to γ: lim eulerMascheroniSeq'(n) = γ.

Русский

Пусть eulerMascheroniSeq' сходится к γ: lim eulerMascheroniSeq'(n) = γ.

LaTeX

$$\lim_{n\to\infty} eulerMascheroniSeq'(n) = \gamma$$

Lean4

theorem tendsto_eulerMascheroniSeq' : Tendsto eulerMascheroniSeq' atTop (𝓝 eulerMascheroniConstant) :=
  by
  suffices Tendsto (fun n ↦ eulerMascheroniSeq' n - eulerMascheroniSeq n) atTop (𝓝 0) by
    simpa using this.add tendsto_eulerMascheroniSeq
  suffices Tendsto (fun x : ℝ ↦ log (x + 1) - log x) atTop (𝓝 0)
    by
    apply (this.comp tendsto_natCast_atTop_atTop).congr'
    filter_upwards [eventually_ne_atTop 0] with n hn
    simp [eulerMascheroniSeq, eulerMascheroniSeq', eq_false_intro hn]
  exact tendsto_log_comp_add_sub_log 1

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