English
Let M and N be positive integers with M dividing N, and χ a Dirichlet character modulo M. If s ∈ C and either χ is nontrivial or s ≠ 1, then the L-function of χ viewed as a Dirichlet character of level N equals the L-function of χ multiplied by the Euler product over primes p dividing the level N: L(s, changeLevel(hMN, χ)) = L(s, χ) · ∏_{p ∈ primeFactors(N)} (1 − χ(p) p^{-s}).
Русский
Пусть M, N ∈ ℕ с M | N и χ — примитивная характер Дирихле по модулю M. Для комплексного числа s и при условии, что либо χ ненулевой, либо s ≠ 1, L-функция χ, трактуемая как характер по модулю N, равна произведению L-функции χ иEuler-произведения по простым p, делящим N: L(s, changeLevel(hMN, χ)) = L(s, χ) · ∏_{p ∈ primeFactors(N)} (1 − χ(p) p^{−s}).
LaTeX
$$$L\bigl(s,\text{changeLevel}(hMN,\chi)\bigr) = L(\chi,s) \cdot \prod_{p \in N.primeFactors} \bigl(1 - \chi(p) \cdot p^{-s}\bigr)$$$
Lean4
/-- If `χ` is a Dirichlet character and its level `M` divides `N`, then we obtain the L function
of `χ` considered as a Dirichlet character of level `N` from the L function of `χ` by multiplying
with `∏ p ∈ N.primeFactors, (1 - χ p * p ^ (-s))`.
(Note that `1 - χ p * p ^ (-s) = 1` when `p` divides `M`). -/
theorem LFunction_changeLevel {M N : ℕ} [NeZero M] [NeZero N] (hMN : M ∣ N) (χ : DirichletCharacter ℂ M) {s : ℂ}
(h : χ ≠ 1 ∨ s ≠ 1) :
LFunction (changeLevel hMN χ) s = LFunction χ s * ∏ p ∈ N.primeFactors, (1 - χ p * p ^ (-s)) :=
by
rcases h with h | h
· have hχ : changeLevel hMN χ ≠ 1 := h ∘ (changeLevel_eq_one_iff hMN).mp
have h' : Continuous fun s ↦ LFunction χ s * ∏ p ∈ N.primeFactors, (1 - χ p * ↑p ^ (-s)) :=
(differentiable_LFunction h).continuous.mul <|
continuous_finset_prod _ fun p hp ↦
by
have : NeZero p := ⟨(Nat.prime_of_mem_primeFactors hp).ne_zero⟩
fun_prop
exact
congrFun
((differentiable_LFunction hχ).continuous.ext_on (dense_compl_singleton 1) h'
(fun _ h ↦ LFunction_changeLevel_aux hMN χ h))
s
· exact LFunction_changeLevel_aux hMN χ h
