infinite series

Stream: mathlib4

[Quinn]

i'm having a lot of trouble doing a simple \Sigma_{t \in \nat}. lsp looks up sigma type / existential quantifier when I ask it to explain the \Sigma symbol, and i've been reading mathlib docs for almost an hour searching

[Quinn]

specifically, I have a proposition on two series u and w, u conv or w div

[Quinn]

why can't i find the function in mathlib that takes functions nat -> R and sends them to ENNReal (simulating taking the sum)? i guess it's not necessarily computable in general (more of a computer algebra problem, anyway) but i feel like i shoudl be able to write it down noncomputationally

[Yaël Dillies]

docs#tsum sounds like what you want

[Quinn]

ah yeah ! that got me much closer.

i'm still not there, because i need to be able to reason about being less than T : ENNReal (top/infintiy) vs being equal to that

[Jireh Loreaux]

docs#Summable f where f : ℕ → ℝ.

[Jireh Loreaux]

If you want ℝ≥0∞-valued things, then maybe you want ∑' n : ℕ, (‖f n‖₊ : ℝ≥0∞). This will be the sum of the absolute value sequence, as an ℝ≥0∞. Whether this value is ∞ or not corresponds to whether or not f is Summable.

[Jireh Loreaux]

the file Mathlib.Analysis.Normed.Group.InfiniteSum has some results of this nature.

[Jireh Loreaux]

There's also docs#ENNReal.tsum_coe_ne_top_iff_summable

[Jireh Loreaux]

@loogle Summable (fun x : ?i ↦ ‖?f x‖₊)

[loogle]

:shrug: nothing found

[Jireh Loreaux]

@Joachim Breitner do you know why this doesn't return docs#Summable.of_nnnorm ?

[Joachim Breitner]

Without deep investigation, if I’d have to guess, probably https://github.com/nomeata/loogle/issues/18