two_mul_riemannZeta_eq_tsum_int_inv_pow_of_even

English

For even k ≥ 2, 2 ζ(k) equals the bilateral sum over integers of (n^k)^{−1}.

Русский

Для чётного k ≥ 2 выполняется равенство 2 ζ(k) = ∑_{n∈ℤ} (n^k)^{−1}.

LaTeX

$$$2 \\\\riemannZeta(k) = \\\\sum_{n \\\\in \\\\mathbb{Z}} ((n)^{k})^{-1}$, with k even and ≥ 2$$

Lean4

theorem two_mul_riemannZeta_eq_tsum_int_inv_pow_of_even {k : ℕ} (hk : 2 ≤ k) (hk2 : Even k) :
    2 * riemannZeta k = ∑' (n : ℤ), ((n : ℂ) ^ k)⁻¹ :=
  by
  have hkk : 1 < k := by linarith
  rw [tsum_int_eq_zero_add_two_mul_tsum_pnat]
  · have h0 : (0 ^ k : ℂ)⁻¹ = 0 := by simp; omega
    norm_cast
    simp [h0, zeta_eq_tsum_one_div_nat_add_one_cpow (s := k) (by simp [hkk]),
      tsum_pnat_eq_tsum_succ (f := fun n => ((n : ℂ) ^ k)⁻¹)]
  · simp [Even.neg_pow hk2]
  · exact (Summable.of_nat_of_neg (by simp [hkk]) (by simp [hkk])).of_norm

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