English
The negative logarithmic derivative of LTrivChar₁ is continuous away from zeros of LTrivChar₁, and globally accounts for poles at s = 1.
Русский
Отрицательная логарифмическая производная LTrivChar₁ непрерывна вне нулей LTrivChar₁ и учитывает пики в s = 1.
LaTeX
$$$\text{ContinuousOn}\left(-\dfrac{\dfrac{d}{ds} LFunctionTrivChar_1(n)(s)}{LFunctionTrivChar_1(n)(s)}\right) \text{ на } \{s : LFunctionTrivChar(n,s) \neq 0\} \cup \{1\}$$$
Lean4
/-- **Functional equation** for primitive Dirichlet L-functions. -/
theorem completedLFunction_one_sub {χ : DirichletCharacter ℂ N} (hχ : IsPrimitive χ) (s : ℂ) :
completedLFunction χ (1 - s) = N ^ (s - 1 / 2) * rootNumber χ * completedLFunction χ⁻¹ s := by
classical
-- First handle special case of Riemann zeta
rcases eq_or_ne N 1 with rfl | hN
·
simp [completedLFunction_modOne_eq, completedRiemannZeta_one_sub, rootNumber_modOne]
-- facts about `χ` as function
have h_sum : ∑ j, χ j = 0 := by
refine χ.sum_eq_zero_of_ne_one (fun h ↦ hN.symm ?_)
rwa [IsPrimitive, h, conductor_one (NeZero.ne _)] at hχ
let ε :=
I ^
(if χ.Even then 0 else 1)
-- gather up powers of N
rw [rootNumber, ← mul_comm_div, ← mul_comm_div, ← cpow_sub _ _ (NeZero.ne _), sub_sub, add_halves]
calc
completedLFunction χ (1 - s)
_ = N ^ (s - 1) * χ (-1) / ε * ZMod.completedLFunction (𝓕 χ) s :=
by
simp only [ε]
split_ifs with h
·
rw [pow_zero, div_one, h, mul_one, completedLFunction,
completedLFunction_one_sub_even h.to_fun _ (.inr h_sum) (.inr <| χ.map_zero' hN)]
· replace h : χ.Odd := χ.even_or_odd.resolve_left h
rw [completedLFunction, completedLFunction_one_sub_odd h.to_fun, pow_one, h, div_I, mul_neg_one, ← neg_mul,
neg_neg]
_ = (_) * ZMod.completedLFunction (fun j ↦ χ⁻¹ (-1) * gaussSum χ stdAddChar * χ⁻¹ j) s :=
by
congr 2 with j
rw [hχ.fourierTransform_eq_inv_mul_gaussSum, ← neg_one_mul j, map_mul, mul_right_comm]
_ = N ^ (s - 1) / ε * gaussSum χ stdAddChar * completedLFunction χ⁻¹ s * (χ (-1) * χ⁻¹ (-1)) :=
by
rw [completedLFunction, completedLFunction_const_mul]
ring
_ = N ^ (s - 1) / ε * gaussSum χ stdAddChar * completedLFunction χ⁻¹ s := by
rw [← MulChar.mul_apply, mul_inv_cancel, MulChar.one_apply (isUnit_one.neg), mul_one]
