English
In the convergent range Re(s) > 1, cosZeta(a)(s) equals the sum over natural n of cos(2π a n)/n^s; i.e., HasSum_{n∈ℕ} cos(2π a n)/n^s = cosZeta(QuotientAddGroup.mk(a))(s).
Русский
В области сходимости Re(s) > 1 косинусная зета равна сумме по натуральным n: HasSum_{n≥0} cos(2π a n)/n^s = cosZeta(Quo(a))(s).
LaTeX
$$$$\\text{HasSum}_{n\\in\\mathbb{N}} \\frac{\\cos(2\\pi a n)}{n^s} = \\cosZeta(\\mathrm{QuotientAddGroup.mk}(a))(s), \\quad 1<\\Re(s).$$$$
Lean4
/-- Formula for `cosZeta` as a Dirichlet series in the convergence range, with sum over `ℕ`. -/
theorem hasSum_nat_cosZeta (a : ℝ) {s : ℂ} (hs : 1 < re s) :
HasSum (fun n : ℕ ↦ Real.cos (2 * π * a * n) / (n : ℂ) ^ s) (cosZeta a s) :=
by
have := (hasSum_int_cosZeta a hs).nat_add_neg
simp_rw [abs_neg, Int.cast_neg, Nat.abs_cast, Int.cast_natCast, mul_neg, abs_zero, Int.cast_zero,
zero_cpow (ne_zero_of_one_lt_re hs), div_zero, zero_div, add_zero, ← add_div, div_right_comm _ _ (2 : ℂ)] at this
simp_rw [push_cast, Complex.cos, neg_mul]
exact this.congr_fun fun n ↦ by rw [show 2 * π * a * n * I = 2 * π * I * a * n by ring]
