English
The auxiliary L-function takes real values for real arguments x > 1; more precisely, it equals its real part for such x.
Русский
Вспомогательная L-функция принимает вещественные значения на вещественных аргументах x > 1; точнее, она равна своей вещественной части на таких x.
LaTeX
$$$LFunctionResidueClassAux(a,x) = \\big(LFunctionResidueClassAux(a,x)\\big)_{\\mathrm{re}} , \\quad x>1$$$
Lean4
/-- The L-series of the von Mangoldt function restricted to the prime residue class `a` mod `q`
is continuous on `re s ≥ 1` except for a simple pole at `s = 1` with residue `(q.totient)⁻¹`.
The statement as given here in terms of `ArithmeticFunction.vonMangoldt.LFunctionResidueClassAux`
is equivalent. -/
theorem continuousOn_LFunctionResidueClassAux : ContinuousOn (LFunctionResidueClassAux a) {s | 1 ≤ s.re} :=
by
refine (continuousOn_LFunctionResidueClassAux' a).mono fun s hs ↦ ?_
rcases eq_or_ne s 1 with rfl | hs₁
· simp only [ne_eq, Set.mem_setOf_eq, true_or]
· simp only [ne_eq, Set.mem_setOf_eq, hs₁, false_or]
exact fun χ ↦ LFunction_ne_zero_of_one_le_re χ (.inr hs₁) <| Set.mem_setOf.mp hs
