English
If Φ is odd, then the completed L-function satisfies a similar functional relation with a factor of i: completedLFunction Φ(1−s) = i · N^{s−1} · completedLFunction(𝓕Φ)(s).
Русский
Если Φ нечетная, то завершённая L-функция удовлетворяет аналогичному функциональному уравнению, но с дополнительным множителем i: completedLFunction Φ(1−s) = i · N^{s−1} · completedLFunction(𝓕Φ)(s).
LaTeX
$$$\mathrm{completedLFunction}(\Phi,1-s) = i \cdot N^{s-1} \cdot \mathrm{completedLFunction}(\mathcal F\Phi, s)$$$
Lean4
/-- Functional equation for completed L-functions (odd case), valid for all `s`. -/
theorem completedLFunction_one_sub_odd (hΦ : Φ.Odd) (s : ℂ) :
completedLFunction Φ (1 - s) = N ^ (s - 1) * I * completedLFunction (𝓕 Φ) s := by
-- This is much easier than the even case since both functions are entire.
-- First set up some notations:
let F (t) := completedLFunction Φ (1 - t)
let G (t) := ↑N ^ (t - 1) * I * completedLFunction (𝓕 Φ) t
have hF : Differentiable ℂ F :=
(differentiable_completedLFunction hΦ.map_zero hΦ.sum_eq_zero).comp (differentiable_id.const_sub 1)
have hG : Differentiable ℂ G :=
by
apply (((differentiable_id.sub_const 1).const_cpow (.inl (NeZero.ne _))).mul_const _).mul
rw [← dft_odd_iff] at hΦ
exact differentiable_completedLFunction hΦ.map_zero hΦ.sum_eq_zero
have : {z | 1 < re z} ∈ 𝓝 2 := (continuous_re.isOpen_preimage _ isOpen_Ioi).mem_nhds (by simp)
have hFG : F =ᶠ[𝓝 2] G := by filter_upwards [this] with t ht using completedLFunction_one_sub_of_one_lt_odd hΦ ht
rw [← analyticOnNhd_univ_iff_differentiable] at hF hG
exact congr_fun (hF.eq_of_eventuallyEq hG hFG) s
