English
The auxiliary L-function is continuous on the set where either the point is 1 or all Dirichlet L-functions do not vanish at that point; in particular it is continuous away from zeros of Dirichlet L-functions and at s = 1.
Русский
Вспомогательная L-функция непрерывна на множестве, состоящем из точек, где либо равенство s = 1, либо все L-функции Дирихле не обращаются к нулю; в частности непрерывна вне нулей Dirichlet L-функций и в окрестности s = 1.
LaTeX
$$$\\mathrm{ContinuousOn}(\\mathrm{LFunctionResidueClassAux}(a))\\{s : \\mathbb{C} \\mid s = 1 \\lor \\forall \\chi:DirichletCharacter(\\mathbb{C},q), LFunction(\\chi)(s) \\neq 0\\}$$$
Lean4
/-- The auxiliary function is continuous away from the zeros of the L-functions of the Dirichlet
characters mod `q` (including at `s = 1`). -/
theorem continuousOn_LFunctionResidueClassAux' :
ContinuousOn (LFunctionResidueClassAux a) {s | s = 1 ∨ ∀ χ : DirichletCharacter ℂ q, LFunction χ s ≠ 0} :=
by
rw [show LFunctionResidueClassAux a = fun s ↦ _ from rfl]
simp only [LFunctionResidueClassAux, sub_eq_add_neg]
refine continuousOn_const.mul <| ContinuousOn.add ?_ ?_
· refine (continuousOn_neg_logDeriv_LFunctionTrivChar₁ q).mono fun s hs ↦ ?_
have := LFunction_ne_zero_of_one_le_re (1 : DirichletCharacter ℂ q) (s := s)
simp only [ne_eq, Set.mem_setOf_eq] at hs
tauto
· simp only [← Finset.sum_neg_distrib, mul_div_assoc, ← mul_neg, ← neg_div]
refine continuousOn_finset_sum _ fun χ hχ ↦ continuousOn_const.mul ?_
replace hχ : χ ≠ 1 := by simpa only [ne_eq, Finset.mem_compl, Finset.mem_singleton] using hχ
refine (continuousOn_neg_logDeriv_LFunction_of_nontriv hχ).mono fun s hs ↦ ?_
simp only [ne_eq, Set.mem_setOf_eq] at hs
rcases hs with rfl | hs
·
simp only [ne_eq, Set.mem_setOf_eq, one_re, le_refl, LFunction_ne_zero_of_one_le_re χ (.inl hχ),
not_false_eq_true]
· exact hs χ
