Monotone convergence for series

Stream: Is there code for X?

[Alex Nguyen]

Is there a monotone convergence theorem for series or a Fatou's lemma for series in mathlib, something along the lines of: https://math.stackexchange.com/questions/2616956/monotone-convergence-theorem-for-series-basic-proof
For a sequence $x_{m n} \geq 0$ if $\lim _{m \rightarrow \infty} x_{m n}=y_n$ (monotonically increasing for $m$ ) then

$\lim _{m \rightarrow \infty} \sum_{n=1}^{\infty} x_{m n}=\sum_{n=1}^{\infty} \lim _{m \rightarrow \infty} x_{m n}$

or Fatou's Lemma for series: If $x_{m n}$ is nonnegative, then

$\sum_{n=1}^{\infty} \liminf _{m \rightarrow \infty} x_{m n} \leqslant \liminf _{m \rightarrow \infty} \sum_{n=1}^{\infty} x_{m n}$

It seems like there's a version tendsto_tsum_of_dominated_convergence for dominated convergence, but I couldn't find one for monotone convergence. Thanks in advance !

[Antoine Chambert-Loir]

The monotone convergence theorem is docs#MeasureTheory.tendsto_of_lintegral_tendsto_of_monotone and there does not seem to have a translation for series in the same way that docs#MeasureTheory.hasSum_integral_of_dominated_convergence translates the general theorem for series.