Source indexedtheorem · leanprover/lean4:v4.32.0

Kadiri.re_tsum_paired_eq_re_inv_add_re_shifted

PrimeNumberTheoremAnd.IEANTN.Kadiri · PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:3077 to 3092

Source documentation

Distributing Re over the packet sum: the paired complex sum splits into the two absolutely summable real-part sums.

Exact Lean statement

theorem re_tsum_paired_eq_re_inv_add_re_shifted (s : ℂ) :
    (∑' ρ : riemannZeta.zeroes_rect (.Ioo 0 1) (.univ : Set ℝ),
        (1 / (ρ.val : ℂ) + 1 / (s - ρ.val))).re =
      (∑' ρ : riemannZeta.zeroes_rect (.Ioo 0 1) (.univ : Set ℝ),
        (1 / (ρ.val : ℂ)).re) +
      ∑' ρ : riemannZeta.zeroes_rect (.Ioo 0 1) (.univ : Set ℝ),
        (1 / (s - ρ.val)).re

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem re_tsum_paired_eq_re_inv_add_re_shifted (s : ℂ) :    (∑' ρ : riemannZeta.zeroes_rect (.Ioo 0 1) (.univ : Set ℝ),        (1 / (ρ.val : ℂ) + 1 / (s - ρ.val))).re =      (∑' ρ : riemannZeta.zeroes_rect (.Ioo 0 1) (.univ : Set ℝ),        (1 / (ρ.val : ℂ)).re) +      ∑' ρ : riemannZeta.zeroes_rect (.Ioo 0 1) (.univ : Set ℝ),        (1 / (s - ρ.val)).re := by  have h1 : (∑' ρ : riemannZeta.zeroes_rect (.Ioo 0 1) (.univ : Set ℝ),      (1 / (ρ.val : ℂ) + 1 / (s - ρ.val))).re =      ∑' ρ : riemannZeta.zeroes_rect (.Ioo 0 1) (.univ : Set ℝ),        (1 / (ρ.val : ℂ) + 1 / (s - ρ.val)).re := by    simpa using ContinuousLinearMap.map_tsum Complex.reCLM      (summable_one_div_add_one_div_at_zeros s)  rw [h1, tsum_congr (fun ρ : riemannZeta.zeroes_rect (.Ioo 0 1) (.univ : Set ℝ) ↦    Complex.add_re (1 / (ρ.val : ℂ)) (1 / (s - ρ.val)))]  exact summable_re_inv_at_zeros.tsum_add (summable_re_one_div_at_zeros s)