tendsto_hurwitzZetaEven_sub_one_div_nhds_one

English

For a real a and s with Re(s) > 1, the Dirichlet series with terms 1/(|n+a|^s)/2 sums to hurwitzZetaEven (a) s.

Русский

Для вещественного a и s с Re(s) > 1 ряд по n∈ℤ вида (1/2)/|n+a|^s суммируется и равен hurwitzZetaEven (a) s.

LaTeX

$$$\\forall a:\\mathbb{R},\\ {s:\\mathbb{C}}\\ (\\Re s>1)\\Rightarrow HasSum\\Bigl(n\\in\\mathbb{Z} \\mapsto \\frac{1}{2}\\,\\frac{\\Gamma(s)}{(|n+a|)^s}\\Bigr)\\ (\\mathrm{hurwitzZetaEven}(a,s)).$$$

Lean4

/-- Expression for `hurwitzZetaEven a 1` as a limit. (Mathematically `hurwitzZetaEven a 1` is
undefined, but our construction assigns some value to it; this lemma is mostly of interest for
determining what that value is). -/
theorem tendsto_hurwitzZetaEven_sub_one_div_nhds_one (a : UnitAddCircle) :
    Tendsto (fun s ↦ hurwitzZetaEven a s - 1 / (s - 1) / Gammaℝ s) (𝓝 1) (𝓝 (hurwitzZetaEven a 1)) := by
  simpa using (differentiableAt_hurwitzZetaEven_sub_one_div a).continuousAt.tendsto

Похожие утверждения