Zulip Chat Archive

Stream: Is there code for X?

Topic: Tail of bounded series tends to zero

view this post on Zulip Markus Himmel (Sep 12 2020 at 15:05):

Does mathlib have a version of the following?

import measure_theory.measure_space

open filter topological_space
open_locale topological_space

lemma tendsto_sum_add (f :   ennreal) (hf : (∑' i, f i) < ) :
  tendsto (λ i, ∑' k, f (i + k)) at_top (𝓝 0) := sorry

view this post on Zulip Heather Macbeth (Sep 12 2020 at 20:15):

There is docs#summable_iff_vanishing_norm . This covers all f : ι → α with α a normed space and with no structure on ι, so it is more general in two ways, but doesn't cover the ennreal part of what you wrote.

Last updated: May 17 2021 at 16:26 UTC