Non-necessarily unconditionally convergent series

Stream: new members

[Gihan Marasingha]

Really basic question, but where are the 'algebra of limits' theorems in mathlib for series in, say, a normed vector space? For instance, where is the theorem that the series of the sum of two convergent series is convergent?

[Johan Commelin]

@Gihan Marasingha

src/topology/algebra/monoid.lean
68:lemma tendsto_mul {a b : M} : tendsto (λp:M×M, p.fst * p.snd) (𝓝 (a, b)) (𝓝 (a * b)) :=

[Patrick Massot]

We have nothing specific for series.

[Patrick Massot]

Of course this doesn't prevent you from getting that the sum of two convergent series is convergent, but this will explicitly be a lemma about their partial sums.

[Patrick Massot]

The main issue is we never decided whether series should be indexed by natural numbers of something more general.

[Frédéric Dupuis]

If you're OK with unconditional convergence only, summable.add and friends in topology/algebra/infinite_sum might suit your purpose.

[Frédéric Dupuis]

Oh, I should have read the title of that post before replying, shouldn't I?