Growth O((σ - 1)⁻¹) from a one-sided limit of (σ - 1) f(σ)

If (σ - 1) f(σ) has a limit as the real variable σ tends to 1 from the right, then f(σ) = O((σ - 1)⁻¹) there. This is how a bound of this shape is usually obtained for a Dedekind zeta function or an L-series near s = 1, from the limit of (s - 1) L(s) along the real axis.

Main results

• TauCeti.isBigO_inv_sub_one_of_tendsto_sub_one_mul: if (σ - 1) f(σ) converges as σ → 1⁺, then f(σ) = O((σ - 1)⁻¹) as σ → 1⁺.

References

• Mathlib's Mathlib/NumberTheory/LSeries/Nonvanishing.lean, by Michael Stoll and David Loeffler, derives the same bound for the Dirichlet L-function of the trivial character in DirichletCharacter.LFunctionTrivChar_isBigO_near_one_horizontal.

theorem TauCeti.isBigO_inv_sub_one_of_tendsto_sub_one_mul {f : ℝ → ℂ} {r : ℂ} (h : Filter.Tendsto (fun (σ : ℝ) => (↑σ - 1) * f σ) (nhdsWithin 1 (Set.Ioi 1)) (nhds r)) : f =O[nhdsWithin 1 (Set.Ioi 1)] fun (σ : ℝ) => (σ - 1)⁻¹

If (σ - 1) f(σ) has a limit as σ → 1⁺ through real values, then f(σ) = O((σ - 1)⁻¹) as σ → 1⁺.