English
A variant of the horizontal big-O bound for the L-function of a Dirichlet character χ: as x → 0^+, LFunction χ(1+x+iy) remains bounded by a constant in the punctured neighborhood, provided the nontriviality condition hy holds.
Русский
Вариант горизонтальной оценки BigO для L-функции χ: при x→0^+, LFunction χ(1+x+iy) остаётся ограниченной в окрестности, за исключением незначимого случая, если соблюдается условие hy.
LaTeX
$$$LFunction(χ,1+x+iy) = O_{nhds^{+}_{0}}(1) \quad (x\to 0^+),$$$
Lean4
theorem LFunction_isBigO_horizontal {y : ℝ} (hy : y ≠ 0 ∨ χ ≠ 1) :
(fun x : ℝ ↦ LFunction χ (1 + x + I * y)) =O[𝓝[>] 0] fun _ ↦ (1 : ℂ) :=
by
refine IsBigO.mono ?_ nhdsWithin_le_nhds
simp_rw [add_comm (1 : ℂ), add_assoc]
have := (χ.differentiableAt_LFunction _ <| one_add_I_mul_ne_one_or χ hy).continuousAt
rw [← zero_add (1 + _)] at this
exact this.comp (f := fun x : ℝ ↦ x + (1 + I * y)) (x := 0) (by fun_prop) |>.tendsto.isBigO_one ℂ
