English
For any Dirichlet character χ modulo N, the L-function along the horizontal line s = 1 + x + i y satisfies a big-O estimate near s with real part 1, providing asymptotic control as x → 0 with y fixed and χ ≠ 1 in the relevant sense.
Русский
Для каждого символа χ по модулю N функция L(χ, s) вдоль горизонтальной линии s = 1 + x + i y удовлетворяет оценке по Большому O близко к s с вещественной частью 1, когда x → 0 при фиксированном y и с учётом условий на χ.
LaTeX
$$$LFunction(χ,1+x+iy) = O(1) \quad \text{при } x \to 0^+,$$$
Lean4
theorem LFunctionTrivChar_isBigO_near_one_horizontal :
(fun x : ℝ ↦ LFunctionTrivChar N (1 + x)) =O[𝓝[>] 0] fun x ↦ (1 : ℂ) / x :=
by
have : (fun w : ℂ ↦ LFunctionTrivChar N (1 + w)) =O[𝓝[≠] 0] (1 / ·) :=
by
have H : Tendsto (fun w ↦ w * LFunctionTrivChar N (1 + w)) (𝓝[≠] 0) (𝓝 <| ∏ p ∈ N.primeFactors, (1 - (p : ℂ)⁻¹)) :=
by
convert (LFunctionTrivChar_residue_one (N := N)).comp (f := fun w ↦ 1 + w) ?_ using 1
· simp only [Function.comp_def, add_sub_cancel_left]
·
simpa only [tendsto_iff_comap, Homeomorph.coe_addLeft, add_zero, map_le_iff_le_comap] using
((Homeomorph.addLeft (1 : ℂ)).map_punctured_nhds_eq 0).le
exact (isBigO_mul_iff_isBigO_div eventually_mem_nhdsWithin).mp <| H.isBigO_one ℂ
exact (isBigO_comp_ofReal_nhds_ne this).mono <| nhdsGT_le_nhdsNE 0
