English
Let a ∈ [0,1] and s ∈ C with Re(s) > 1. Then the series ∑_{n≥0} 1/(n + a)^s converges and equals the Hurwitz zeta function HurwitzZeta(a, s).
Русский
Пусть a ∈ [0,1] и s ∈ C с Re(s) > 1. Тогда ряд ∑_{n≥0} 1/(n + a)^s сходится и равен HurwitzZeta(a, s).
LaTeX
$$$\\displaystyle \\sum_{n=0}^{\\infty} \\frac{1}{(n+a)^s} = \\operatorname{HurwitzZeta}(a,s), \\quad a \\in [0,1], \\quad \\operatorname{Re}(s) > 1.$$$
Lean4
/-- Formula for `hurwitzZeta s` as a Dirichlet series in the convergence range. We
restrict to `a ∈ Icc 0 1` to simplify the statement. -/
theorem hasSum_hurwitzZeta_of_one_lt_re {a : ℝ} (ha : a ∈ Icc 0 1) {s : ℂ} (hs : 1 < re s) :
HasSum (fun n : ℕ ↦ 1 / (n + a : ℂ) ^ s) (hurwitzZeta a s) :=
by
convert (hasSum_nat_hurwitzZetaEven_of_mem_Icc ha hs).add (hasSum_nat_hurwitzZetaOdd_of_mem_Icc ha hs) using 1
ext1 n
apply show ∀ (x y : ℂ), x = (x + y) / 2 + (x - y) / 2 by intros; ring
