Source indexedlemma · leanprover/lean4:v4.32.0

finsetSum_tendsto_tsum

PrimeNumberTheoremAnd.ZetaBounds · PrimeNumberTheoremAnd/ZetaBounds.lean:901 to 911

Mathematical statement

Exact Lean statement

lemma finsetSum_tendsto_tsum {N : ℕ} {f : ℕ → ℂ} (hf : Summable f) :
    Tendsto (fun (k : ℕ) ↦ ∑ n ∈ Finset.Ico N k, f n) atTop (𝓝 (∑' (n : ℕ), f (n + N)))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma finsetSum_tendsto_tsum {N : ℕ} {f : ℕ → ℂ} (hf : Summable f) :    Tendsto (fun (k : ℕ) ↦ ∑ n ∈ Finset.Ico N k, f n) atTop (𝓝 (∑' (n : ℕ), f (n + N))) := by  have := Summable.hasSum_iff_tendsto_nat hf (m := ∑' (n : ℕ), f n) |>.mp hf.hasSum  have const := tendsto_const_nhds (α := ℕ) (x := ∑ i ∈ Finset.range N, f i) (f := atTop)  have := Filter.Tendsto.sub this const  rw [← hf.sum_add_tsum_nat_add N, add_comm, add_sub_cancel_right] at this  apply this.congr'  filter_upwards [Filter.mem_atTop (N + 1)]  intro M hM  rw [Finset.sum_Ico_eq_sub]  linarith