English
The completed zeta function equals the Dirichlet series with a gamma factor: completedZeta(s) = π^{−s/2} Γ(s/2) ∑_{n≥1} n^{−s} for Re(s) > 1.
Русский
Оконченная дзета равна дзете по Дирихле умноженной на гамма-фактор: \\\\hat{ζ}(s) = π^{−s/2} Γ(s/2) ∑_{n≥1} n^{−s}, при Re(s) > 1.
LaTeX
$$$\\\\hat{\\\\zeta}(s) = π^{-s/2} Γ(s/2) \\\\sum_{n=1}^{∞} n^{-s}$, 1 < Re(s)$$
Lean4
theorem completedZeta_eq_tsum_of_one_lt_re {s : ℂ} (hs : 1 < re s) :
completedRiemannZeta s = (π : ℂ) ^ (-s / 2) * Gamma (s / 2) * ∑' n : ℕ, 1 / (n : ℂ) ^ s :=
by
have := (hasSum_nat_completedCosZeta 0 hs).tsum_eq.symm
simp only [QuotientAddGroup.mk_zero, completedCosZeta_zero] at this
simp only [this, Gammaℝ_def, mul_zero, zero_mul, Real.cos_zero, ofReal_one, mul_one, mul_one_div, ← tsum_mul_left]
congr 1 with n
split_ifs with h
· simp only [h, Nat.cast_zero, zero_cpow (Complex.ne_zero_of_one_lt_re hs), div_zero]
· rfl
