LSeriesHasSum_exp — Mathlib

English

ExpZeta is the meromorphic continuation of the series ∑' e^{2π i a n}/n^s; equivalently, ExpZeta(a,s) = cosZeta(a,s) + i sinZeta(a,s).

Русский

ExpZeta — мероморфное продолжение ряда ∑' e^{2π i a n}/n^s; эквивалентно ExpZeta(a,s) = cosZeta(a,s) + i sinZeta(a,s).

LaTeX

$$$\\displaystyle \\expZeta(a,s) = \\cosZeta(a,s) + i\, \\sinZeta(a,s).$$$

Lean4

/-- Reformulation of `hasSum_expZeta_of_one_lt_re` using `LSeriesHasSum`. -/
theorem LSeriesHasSum_exp (a : ℝ) {s : ℂ} (hs : 1 < re s) : LSeriesHasSum (cexp <| 2 * π * I * a * ·) s (expZeta a s) :=
  (hasSum_expZeta_of_one_lt_re a hs).congr_fun (LSeries.term_of_ne_zero' (ne_zero_of_one_lt_re hs) _)

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