LSeriesHasSum_sin — Mathlib

English

For a ∈ ℝ and s with Re(s) > 1, the L-series with coefficients sin(2π a n) converges to sinZeta(a, s); that is, LSeriesHasSum(sin(2π a x)) = sinZeta(a, s).

Русский

Для a∈ℝ и Re(s)>1, L-ряд со степенными коэффициентами sin(2π a n) сходится к sinZeta(a, s).

LaTeX

$$$$ \text{LSeriesHasSum}_{n\ge 0}(\operatorname{sin}(2\pi a n), s) = \sinZeta(a,s). $$$$

Lean4

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

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