hasSum_expZeta_of_one_lt_re — Mathlib

English

For Re(s) > 1 and a ∈ ℝ, the Dirichlet-type series ∑_{n≥1} e^{2π i a n}/n^s converges to expZeta(a,s).

Русский

При Re(s) > 1 и a ∈ ℝ ряд ∑_{n≥1} e^{2π i a n}/n^s сходится к expZeta(a,s).

LaTeX

$$$$\\sum_{n=1}^{\\infty} \\frac{e^{2\\pi i a n}}{n^{s}} = \\expZeta(a,s), \\quad \\operatorname{Re}(s) > 1, \\ a\\in\\mathbb{R}.$$$$

Lean4

theorem hasSum_expZeta_of_one_lt_re (a : ℝ) {s : ℂ} (hs : 1 < re s) :
    HasSum (fun n : ℕ ↦ cexp (2 * π * I * a * n) / n ^ s) (expZeta a s) :=
  by
  convert (hasSum_nat_cosZeta a hs).add ((hasSum_nat_sinZeta a hs).mul_left I) using 1
  ext1 n
  simp only [mul_right_comm _ I, ← cos_add_sin_I, push_cast]
  rw [add_div, mul_div, mul_comm _ I]

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