English
If 1 < Re(s), the congruence L-function agrees with the Dirichlet series: LFunction Φ s = LSeries (Φ ·) s.
Русский
При 1 < Re(s) конгруэнтная L-функция совпадает с ряда Дирихле: LFunction Φ s = LSeries (Φ ·) s.
LaTeX
$$$$L(\Phi, s) = L_{\mathrm{Dir}}(\Phi, s) \quad \text{for } \operatorname{Re}(s) > 1.$$$$
Lean4
/-- For `1 < re s` the congruence L-function agrees with the sum of the Dirichlet series. -/
theorem LFunction_eq_LSeries (Φ : ZMod N → ℂ) {s : ℂ} (hs : 1 < re s) : LFunction Φ s = LSeries (Φ ·) s :=
by
rw [LFunction, LSeries, mul_sum, Nat.sumByResidueClasses (LSeriesSummable_of_one_lt_re Φ hs) N]
congr 1 with j
have : (j.val / N : ℝ) ∈ Set.Icc 0 1 :=
mem_Icc.mpr ⟨by positivity, (div_le_one (Nat.cast_pos.mpr <| NeZero.pos _)).mpr <| Nat.cast_le.mpr (val_lt j).le⟩
rw [toAddCircle_apply, ← (hasSum_hurwitzZeta_of_one_lt_re this hs).tsum_eq, ← mul_assoc, ← tsum_mul_left]
congr 1 with m
calc
N ^ (-s) * Φ j * (1 / (m + (j.val / N : ℝ)) ^ s)
_ = Φ j * (N ^ (-s) * (1 / (m + (j.val / N : ℝ)) ^ s)) := by rw [← mul_assoc, mul_comm _ (Φ _)]
_ = Φ j * (1 / (N : ℝ) ^ s * (1 / ((j.val + N * m) / N : ℝ) ^ s)) := by
simp only [cpow_neg, ← one_div, ofReal_div, ofReal_natCast, add_comm, add_div, ofReal_add, ofReal_mul,
mul_div_cancel_left₀ (m : ℂ) (Nat.cast_ne_zero.mpr (NeZero.ne N))]
_ = Φ j / ((N : ℝ) * ((j.val + N * m) / N : ℝ)) ^ s := by -- this is the delicate step!
rw [one_div_mul_one_div, mul_one_div, mul_cpow_ofReal_nonneg] <;> positivity
_ = Φ j / (N * (j.val + N * m) / N) ^ s := by
simp only [ofReal_natCast, ofReal_div, ofReal_add, ofReal_mul, mul_div_assoc]
_ = Φ j / (j.val + N * m) ^ s := by rw [mul_div_cancel_left₀ _ (Nat.cast_ne_zero.mpr (NeZero.ne N))]
_ = Φ ↑(j.val + N * m) / (↑(j.val + N * m)) ^ s := by
simp only [Nat.cast_add, Nat.cast_mul, natCast_zmod_val, natCast_self, zero_mul, add_zero]
_ = LSeries.term (Φ ·) s (j.val + N * m) := by rw [LSeries.term_of_ne_zero' (ne_zero_of_one_lt_re hs)]
