LSeriesHasSum_cos — Mathlib

English

Reformulating the natural-Dirichlet cosZeta sum, one obtains an L-series interpretation: LSeriesHasSum(cos(2π a x)) s = cosZeta(a)(s) for Re(s) > 1.

Русский

Переформулируя сумму cosZeta через ряд Ли, получаем трактовку L-серии: LSeriesHasSum(cos(2π a x)) s = cosZeta(a)(s) при Re(s) > 1.

LaTeX

$$$$\\text{LSeriesHasSum}(\\cos(2\\pi a x), s) = \\cosZeta(a)(s), \\quad \\Re(s)>1.$$$$

Lean4

/-- Reformulation of `hasSum_nat_cosZeta` using `LSeriesHasSum`. -/
theorem LSeriesHasSum_cos (a : ℝ) {s : ℂ} (hs : 1 < re s) : LSeriesHasSum (Real.cos <| 2 * π * a * ·) s (cosZeta a s) :=
  (hasSum_nat_cosZeta a hs).congr_fun (LSeries.term_of_ne_zero' (ne_zero_of_one_lt_re hs) _)

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