Source indexedlemma · leanprover/lean4:v4.32.0

ZetaSum_aux3

PrimeNumberTheoremAnd.ZetaBounds · PrimeNumberTheoremAnd/ZetaBounds.lean:931 to 941

Mathematical statement

Exact Lean statement

lemma ZetaSum_aux3 {N : ℕ} {s : ℂ} (s_re_gt : 1 < s.re) :
    Tendsto (fun k ↦ ∑ n ∈ Finset.Ioc N k, 1 / (n : ℂ) ^ s) atTop
    (𝓝 (∑' (n : ℕ), 1 / (n + N + 1 : ℂ) ^ s))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma ZetaSum_aux3 {N : ℕ} {s : ℂ} (s_re_gt : 1 < s.re) :    Tendsto (fun k ↦ ∑ n ∈ Finset.Ioc N k, 1 / (n : ℂ) ^ s) atTop    (𝓝 (∑' (n : ℕ), 1 / (n + N + 1 : ℂ) ^ s)) := by  let f := fun (n : ℕ) ↦ 1 / (n : ℂ) ^ s  have hf := summable_one_div_nat_cpow.mpr s_re_gt  simp_rw [Finset.Ioc_eq_Ico]  convert finsetSum_tendsto_tsum (f := fun n ↦ f (n + 1)) (N := N) ?_ using 1  · ext k    rw [Finset.sum_Ico_add']  · congr; ext n; simp only [one_div, Nat.cast_add, Nat.cast_one, f]  · rwa [summable_nat_add_iff (k := 1)]