English
A functional equation for L-functions: L(Φ, 1−s) equals N^(s−1)(2π)^(−s)Γ(s) times a linear combination of L(𝓕Φ, s) and L(𝓕(Φ(−·)), s) with exponential factors.
Русский
Функциональное уравнение L-функций: L(Φ, 1−s) равняется N^(s−1)(2π)^(−s)Γ(s) умножить на линейную комбинацию L(𝓕Φ, s) и L(𝓕(Φ(−·)), s) с коэффициентами экспонент.
LaTeX
$$$$L(\Phi, 1-s) = N^{s-1} (2\pi)^{-s} \Gamma(s) \Big( e^{\pi i s/2} L(\mathcal{F}\Phi, s) + e^{-\pi i s/2} L(\mathcal{F}(\Phi(-\cdot)), s) \Big).$$$$
Lean4
/-- Functional equation for `ZMod` L-functions, in terms of discrete Fourier transform. -/
theorem LFunction_one_sub (Φ : ZMod N → ℂ) {s : ℂ} (hs : ∀ (n : ℕ), s ≠ -n) (hs' : Φ 0 = 0 ∨ s ≠ 1) :
LFunction Φ (1 - s) =
N ^ (s - 1) * (2 * π) ^ (-s) * Gamma s *
(cexp (π * I * s / 2) * LFunction (𝓕 Φ) s + cexp (-π * I * s / 2) * LFunction (𝓕 fun x ↦ Φ (-x)) s) :=
by
rw [LFunction]
have (j : ZMod N) :
Φ j * hurwitzZeta (toAddCircle j) (1 - s) =
Φ j *
((2 * π) ^ (-s) * Gamma s *
(cexp (-π * I * s / 2) * expZeta (toAddCircle j) s + cexp (π * I * s / 2) * expZeta (-toAddCircle j) s)) :=
by
rcases eq_or_ne j 0 with rfl | hj
· rcases hs' with hΦ | hs'
· simp only [hΦ, zero_mul]
· rw [hurwitzZeta_one_sub _ hs (Or.inr hs')]
· rw [hurwitzZeta_one_sub _ hs (Or.inl <| toAddCircle_eq_zero.not.mpr hj)]
simp only [this, mul_assoc _ _ (Gamma s)]
-- get rid of Gamma terms and power of N
generalize (2 * π) ^ (-s) * Gamma s = C
simp_rw [← mul_assoc, mul_comm _ C, mul_assoc, ← mul_sum, ← mul_assoc, mul_comm _ C, mul_assoc, neg_sub]
congr 2
-- now gather sum terms
rw [LFunction_dft _ hs', LFunction_dft _ (hs'.imp_left <| by simp only [neg_zero, imp_self])]
conv_rhs => enter [2, 2]; rw [← (Equiv.neg _).sum_comp _ _ (by simp), Equiv.neg_apply]
simp_rw [neg_neg, mul_sum, ← sum_add_distrib, ← mul_assoc, mul_comm _ (Φ _), mul_assoc, ← mul_add, map_neg, add_comm]
