isBigO_riemannZeta_sub_one_div — Mathlib

English

The growth of riemannZeta(s) - 1/(s-1) is bounded by a constant near s = 1, i.e., it is O(1) as s → 1.

Русский

Рост riemannZeta(s) - 1/(s-1) близко к s = 1 ограничен константой, т.е. имеет порядок O(1) при s→1.

LaTeX

$$$$(\\\\operatorname{riemannZeta}(s) - \\\\frac{1}{s-1}) =O_{\\\\nhds 1}(1)$$$$

Lean4

theorem _root_.isBigO_riemannZeta_sub_one_div {F : Type*} [Norm F] [One F] [NormOneClass F] :
    (fun s : ℂ ↦ riemannZeta s - 1 / (s - 1)) =O[𝓝 1] (fun _ ↦ 1 : ℂ → F) := by
  simpa only [Asymptotics.isBigO_one_nhds_ne_iff] using tendsto_riemannZeta_sub_one_div.isBigO_one (F := F)

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