Stolz–Cesàro theorem

Stream: Is there code for X?

[Alex Kontorovich]

Do we have something like this? https://en.wikipedia.org/wiki/Stolz%E2%80%93Ces%C3%A0ro_theorem I would think this belongs in a similar place to things like docs#Filter.Tendsto.cesaro but didn't find it? Thanks!

[Antoine Chambert-Loir]

(I didn't know that theorem. The applications given in Wikipedia are however absurd since they follow from the classical Cesàro summation result… For what cases would you want to use it? — The proof given at the end of the Wikipedia article you mention is remarkably concise.)

[Alex Kontorovich]

For example, it is used to show things like: if $|a_{n+1}|/|a_n|$ has limit $L$, then so does $|a_n|^{1/n}$. (This is a standard exercise in, e.g., Rudin, and may itself have further applications...)

[Antoine Chambert-Loir]

But you don't need it for this particular case. After passing to log, classical Cesaro is enough since it says that if $a_n \to l$, then $(a_1+\dots+a_n)/n \to l$.

[Antoine Chambert-Loir]

(And this case is probably present in Mathlib when it talks about radius of convergence…)

[Alex Kontorovich]

Yes in fact that was the use case, Hadamard's formula for radius of convergence. I didn't see it in Mathlib - could you please point me?

[Jireh Loreaux]

docs#FormalMultilinearSeries.radius_eq_liminf