Is Stolz–Cesàro theorem formalized in mathlib?

Stream: mathlib4

[Planck Anderson]

Hi all,

I was wondering whether the Stolz–Cesàro theorem has been formalized in mathlib4 yet. I searched but couldn't find anything like stolz, cesaro, or relevant lemmas involving difference quotients of sequences.

To clarify, I’m referring to the version that says:

If $b_n$ is strictly increasing and tends to $+\infty$, and if

$$\lim_{n \to \infty} \frac{a_{n+1} - a_n}{b_{n+1} - b_n} = L$$

then

$$\lim_{n \to \infty} \frac{a_n}{b_n} = L.$$

Has this been proven or is anyone working on it?

[Sébastien Gouëzel]

We have docs#Filter.Tendsto.cesaro and docs#Filter.Tendsto.cesaro_smul (which are the classical version for b_n = n), but probably not the version you're mentioning (although the proof won't be really different).

[Sébastien Gouëzel]

(The main lemma in our proof is docs#Asymptotics.IsLittleO.sum_range, which is also suitable for your statement)

[Planck Anderson]

Hi Sébastien, thanks a lot for the detailed response!

My math background is still not very strong, and I'm not yet familiar with how to use the tools you mentioned to prove this version of the theorem.
So far I only know how to prove the Stolz–Cesàro theorem using the classical $\varepsilon$ – $N$ language, i.e.,

$$\lim_{n \to \infty} a_n = L \quad \Longleftrightarrow \quad \forall \varepsilon > 0,\ \exists N \in \mathbb{N},\ \forall n \ge N,\ |a_n - L| < \varepsilon.$$

But I’ll try to understand how to approach it using the Filter framework now — really appreciate the guidance!

[Sébastien Gouëzel]

The $\epsilon-N$ approach is exactly what is done in the proof of docs#Asymptotics.IsLittleO.sum_range, there's no way around it in this proof. But it has already been done for you there, you just need to apply the lemma now.

[Planck Anderson]

Thanks for the reply!

How about the version of the Stolz–Cesàro theorem I’m referring to is the one usually proven in undergraduate real analysis using an ε–N argument. Below is the version and proof I mean, presented in full detail:

Let $\{y_n\}$ be a strictly increasing sequence tending to $+\infty$, and suppose

$$\lim_{n \to \infty} \frac{x_n - x_{n-1}}{y_n - y_{n-1}} = a, \quad \text{for } -\infty \le a \le +\infty,$$

then we have

$$\lim_{n \to \infty} \frac{x_n}{y_n} = a.$$

The proof I’m following goes like this:

• First prove the case $a = 0$:

For any $\varepsilon > 0$, there exists $N$ such that for all $n > N$,

$$|x_n - x_{n-1}| < \varepsilon (y_n - y_{n-1}).$$

Summing up, we get:

$$|x_n - x_N| < \varepsilon (y_n - y_N).$$

Dividing both sides by $y_n$ and letting $n \to \infty$ gives:

$$\left| \frac{x_n}{y_n} - \frac{x_N}{y_n} \right| < \varepsilon \left( 1 - \frac{y_N}{y_n} \right) \to \varepsilon.$$

Hence $\lim_{n \to \infty} \frac{x_n}{y_n} = 0$.

• For general $a \in \mathbb{R}$, let $x_n' = x_n - a y_n$. Then

$$\lim_{n \to \infty} \frac{x_n'}{y_n} = \lim_{n \to \infty} \left( \frac{x_n}{y_n} - a \right),$$

and we reduce to the $a = 0$ case again.

• For $a = +\infty$, one shows that

$$\frac{x_n - x_{n-1}}{y_n - y_{n-1}} > G$$

for any $G > 0$, eventually in $n$, which implies $x_n$ is also strictly increasing and diverges to $+\infty$.

I will try to read docs#Asymptotics.IsLittleO.sum_range and prove it. And I also wanna try something like I mentioned~

[Kenny Lau]

@Planck Anderson well if there's a relevant lemma then you should always use it, in mathlib you shouldn't have to prove a lot of things from scratch

[Planck Anderson]

thanks a lot, I just found that docs#Asymptotics.IsLittleO.sum_range was really useful!!