tendsto_harmonic_sub_log — Mathlib

English

The sequence H_n − log n converges to γ: lim_{n→∞} (H_n − log n) = γ.

Русский

Последовательность H_n − log n сходится к γ: lim_{n→∞} (H_n − log n) = γ.

LaTeX

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

Lean4

theorem tendsto_harmonic_sub_log : Tendsto (fun n : ℕ ↦ harmonic n - log n) atTop (𝓝 eulerMascheroniConstant) :=
  by
  apply tendsto_eulerMascheroniSeq'.congr'
  filter_upwards [eventually_ne_atTop 0] with n hn
  simp_rw [eulerMascheroniSeq', hn, if_false]

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