English
For a primitive χ, the completed L-function satisfies the functional equation: completedLFunction(χ,1−s) = N^{s−1/2} rootNumber(χ) completedLFunction(χ^{-1}, s).
Русский
Для примитивного χ выполняется функциональное уравнение: завершённаяL-функция χ(1−s) = N^{s−1/2} rootNumber(χ) завершённаяL-функция χ^{-1}(s).
LaTeX
$$$\text{completedLFunction}(\chi,1-s) = N^{s-1/2} \cdot \text{rootNumber}(\chi) \cdot \text{completedLFunction}(\chi^{-1},s)$$$
Lean4
/-- The negative logarithmic derivative of `s ↦ (s - 1) * L χ s` for a trivial
Dirichlet character `χ` is continuous away from the zeros of `L χ` (including at `s = 1`). -/
theorem continuousOn_neg_logDeriv_LFunctionTrivChar₁ :
ContinuousOn (fun s ↦ -deriv (LFunctionTrivChar₁ n) s / LFunctionTrivChar₁ n s)
{s | s = 1 ∨ LFunctionTrivChar n s ≠ 0} :=
by
simp_rw [neg_div]
have h := differentiable_LFunctionTrivChar₁ n
refine ((h.contDiff.continuous_deriv le_rfl).continuousOn.div h.continuous.continuousOn fun w hw ↦ ?_).neg
rcases eq_or_ne w 1 with rfl | hw'
· exact LFunctionTrivChar₁_apply_one_ne_zero _
· rw [LFunctionTrivChar₁, Function.update_of_ne hw', mul_ne_zero_iff]
exact ⟨sub_ne_zero_of_ne hw', (Set.mem_setOf.mp hw).resolve_left hw'⟩
