Stream: Is there code for X?
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
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