TheoremStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-27

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Stolz-Cesaro, $\infty / \infty$ form: if $b_{k}$ is strictly increasing and unbounded and $(a_{k + 1} - a_{k}) / (b_{k + 1} - b_{k}) \to L$ then $a_{k} / b_{k} \to L$

Statement

Let $(a_{k})$ and $(b_{k})$ be sequences of reals (Sequences of reals: bounded, eventually, frequently, tails, subsequences) such that $(b_{k})$ is strictly increasing (Nondecreasing, increasing, nonincreasing, decreasing, monotone, and eventually monotone sequences) and its range is not bounded above (Lower bound, bounded below, bounded set). Then $b_{k + 1} - b_{k} > 0$ for every $k$ , so the difference quotient

$d_{k} : = \frac{a_{k + 1} - a_{k}}{b_{k + 1} - b_{k}}$

is defined for every $k \in N$ . Suppose $(d_{k})$ converges.

Then there is $K_{0} \in N$ with $b_{k} > 0$ for every $k \geq K_{0}$ , so that $q_{j} : = a_{j + K_{0}} / b_{j + K_{0}}$ is a sequence of reals; that sequence converges, and

$\lim_{j} q_{j} = \lim_{k} d_{k} .$

Both limits are asserted to exist: the right-hand one by hypothesis, the left-hand one as part of the conclusion. If moreover $b_{k} \neq 0$ for every $k$ , so that $(a_{k} / b_{k})$ is itself a sequence of reals, then it converges and $\lim_{k} a_{k} / b_{k} = \lim_{k} d_{k}$ , because convergence depends only on a tail (Convergence depends only on the tail).

Why the statement is about a tail. Nothing forbids $b_{0} = 0$ , and the two standard applications on the companion examples page have exactly that, $b_{k} = k$ in one and $b_{n} = n^{p + 1}$ in the other. Writing the conclusion for the whole sequence would be writing a quotient that does not denote at $k = 0$ .

The notation is licensed by uniqueness of limits of real sequences (A sequence has at most one limit).

Facts & Assumptions

Given: Sequences $(a_{k})$ , $(b_{k})$ of reals with $(b_{k})$ strictly increasing and with range not bounded above, and the difference quotients $d_{k} = (a_{k + 1} - a_{k}) / (b_{k + 1} - b_{k})$ , assumed to converge; write $L : = \lim_{k} d_{k}$ .

[L1]

Sequences, tails and strict monotonicity: $(b_{k})$ strictly increasing means $b_{j} < b_{k}$ for $j < k$ , so $b_{k + 1} - b_{k} > 0$ (Sequences of reals: bounded, eventually, frequently, tails, subsequences, Nondecreasing, increasing, nonincreasing, decreasing, monotone, and eventually monotone sequences).

[L2]

Not bounded above: no real is $\geq$ every element of the range (Lower bound, bounded below, bounded set).

[L3]

A nondecreasing sequence whose range is not bounded above diverges to $+ \infty$ , that is, for every real $M$ there is $K$ with $b_{k} > M$ for all $k \geq K$ (A nondecreasing sequence that is not bounded above diverges to $+ \infty$ , Divergence to $+ \infty$ and to $- \infty$ ).

[L4]

Finite sums (Finite sums and finite products, by recursion) and their laws: telescoping $\sum_{k < n} (c_{k + 1} - c_{k}) = c_{n} - c_{0}$ , splitting, additivity, scaling and monotonicity in the terms (Laws of finite sums and finite products).

[L5]

Triangle inequalities: $∣ \sum_{k < n} u_{k} ∣ \leq \sum_{k < n} ∣ u_{k} ∣$ (Triangle inequality for finite sums) and $∣ u + v ∣ \leq ∣ u ∣ + ∣ v ∣$ (The triangle inequality); also $∣ u v ∣ = ∣ u ∣ ∣ v ∣$ and $∣ u ∣ = u$ for $u \geq 0$ (Basic properties of the absolute value).

[L6]

Convergence: for every real $ε > 0$ there is $K$ beyond which the terms are within $ε$ of the limit, the rational and real formulations agreeing (Limits and Cauchy sequences of reals, Sequences of reals: bounded, eventually, frequently, tails, subsequences, The rationals embed densely in the reals); limits are unique (A sequence has at most one limit).

[L7]

For a sequence of strictly positive reals, converging to $0$ is equivalent to the reciprocal sequence diverging to $+ \infty$ (For positive terms, null and divergence to $+ \infty$ are reciprocal).

[L8]

Convergence depends only on the tail (Convergence depends only on the tail).

[L9]

Algebra of limits: a scalar multiple of a convergent sequence converges to the scalar multiple of the limit (Algebra of limits: sums, scalar multiples, products and quotients).

[L10]

Order arithmetic: $a > 0$ gives $a^{- 1} > 0$ and $0 < a < b$ gives $0 < b^{- 1} < a^{- 1}$ (Inverses of positives are positive, and reciprocation reverses order); for $c > 0$ , $a < b$ if and only if $a c < b c$ (Sign rules for products and monotonicity of multiplication); adding a constant preserves the order and inequalities add (Order is preserved by adding a constant and by adding inequalities); the order is total and transitive (Complete ordered field (least-upper-bound property), Ordered field); and of two indices one is the larger ( $\leq$ is a linear order on $N$ ).

Proof

technique · direct

1.1

$(b_{k})$ is nondecreasing and its range is not bounded above, so it diverges to $+ \infty$ ; taking $M = 0$ gives $K_{0} \in N$ with $b_{k} > 0$ for every $k \geq K_{0}$ , and then $q_{j} : = a_{j + K_{0}} / b_{j + K_{0}}$ is a well-defined sequence of reals.

L1L2L3L10

1.2

For every $k$ one has $b_{k + 1} - b_{k} > 0$ , so each $d_{k}$ is defined and $a_{k + 1} - a_{k} = d_{k} (b_{k + 1} - b_{k})$ .

L1L10

2.1

For all $K < n$ : telescoping gives $a_{n} - a_{K} = \sum_{k = K}^{n - 1} (a_{k + 1} - a_{k}) = \sum_{k = K}^{n - 1} d_{k} (b_{k + 1} - b_{k})$ and $b_{n} - b_{K} = \sum_{k = K}^{n - 1} (b_{k + 1} - b_{k})$ , hence $a_{n} - a_{K} - L (b_{n} - b_{K}) = \sum_{k = K}^{n - 1} (d_{k} - L) (b_{k + 1} - b_{k})$ .

step 1.2L4

2.2

Let $ε > 0$ be an arbitrary real; choose $K \geq K_{0}$ with $∣ d_{k} - L ∣ < ε / 2$ for every $k \geq K$ .

step 1.1L6L10choose

3.1

For every $n > K$ : $∣ a_{n} - a_{K} - L (b_{n} - b_{K}) ∣ \leq \sum_{k = K}^{n - 1} ∣ d_{k} - L ∣ (b_{k + 1} - b_{k}) \leq (ε / 2) (b_{n} - b_{K})$ , and $b_{K} > 0$ with $b_{n} > b_{K}$ gives $0 < b_{n} - b_{K} < b_{n}$ , so dividing by $b_{n} > 0$ yields $∣ a_{n} / b_{n} - L - (a_{K} - L b_{K}) / b_{n} ∣ < ε / 2$ and therefore $∣ a_{n} / b_{n} - L ∣ < ε / 2 + ∣ a_{K} - L b_{K} ∣ / b_{n}$ .

step 2.1step 2.2L4L5L10

3.2

The sequence $j \mapsto 1 / b_{j + K_{0}}$ has strictly positive terms and its reciprocal $j \mapsto b_{j + K_{0}}$ diverges to $+ \infty$ , so it converges to $0$ ; multiplying by the constant $∣ a_{K} - L b_{K} ∣$ , the sequence $j \mapsto ∣ a_{K} - L b_{K} ∣ / b_{j + K_{0}}$ converges to $0$ .

step 1.1step 2.2L3L7L9

4.1

So there is $N \geq K$ with $∣ a_{K} - L b_{K} ∣ / b_{n} < ε / 2$ for every $n \geq N$ , and then $∣ a_{n} / b_{n} - L ∣ < ε / 2 + ε / 2 = ε$ for every $n \geq N$ ; equivalently $∣ q_{j} - L ∣ < ε$ for every $j \geq N - K_{0}$ .

step 3.1step 3.2L6L10

5.1

As $ε > 0$ was arbitrary, $(q_{j})$ converges to $L$ , so $\lim_{j} q_{j}$ exists and equals $L = \lim_{k} d_{k}$ ; and if $b_{k} \neq 0$ for every $k$ then $(a_{k} / b_{k})$ is a sequence of reals whose $K_{0}$ -th tail is $(q_{j})$ , so it too converges to $L$ .

step 4.1L6L8∎

Remarks

This is a discrete l'Hopital rule, and the shape of the proof says why: the increments of $a$ are compared with the increments of $b$ , the comparison is summed by telescoping, and the fixed head $a_{K} - L b_{K}$ is washed out by the divergence of $b_{n}$ . The head is exactly the constant of integration.
Strict increase is used twice, once so that $b_{k + 1} - b_{k} \neq 0$ and the quotients $d_{k}$ exist, and once so that $b_{n} - b_{K} > 0$ and the sum estimate keeps its sign. Unboundedness is used twice as well, once to reach positive $b_{k}$ and once to kill the head.
There is no converse, not even under the same hypotheses: $a_{k} = (- 1)^{k}$ , $b_{k} = k$ have $a_{k} / b_{k} \to 0$ while the difference quotient oscillates, so Stolz-Cesaro has no converse ↗ exhibits $a_{k}$ and $b_{k}$ for which $a_{k} / b_{k}$ converges while $(d_{k})$ oscillates between two values.
The Cesaro mean theorem is the special case $a_{n} = \sum_{k = 0}^{n} x_{k}$ , $b_{n} = n + 1$ : then $d_{n} = x_{n + 1}$ , and the conclusion reads $σ_{n} \to \lim_{k} x_{k}$ . That deduction is not carried out here, because If $x_{k} \to L$ then $σ_{n} \to L$ : convergence implies $(C, 1)$ -summability to the same value is proved directly and earlier; the observation is recorded so the reader can see the two results are one.

Depends on

Used by

Dependency tree · two levels

54 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Stolz-Cesàro theorem (Wikipedia) (standard reference, not scraped)
Cesàro summation (Wikipedia) (standard reference, not scraped)
J. Lebl, Basic Analysis I, §2.2 and §2.3 (standard reference, not scraped)

Stolz-Cesaro, ∞/∞∞/∞ form: if bkbk​ is strictly increasing and unbounded and (ak+1−ak)/(bk+1−bk)→L(ak+1​−ak​)/(bk+1​−bk​)→L then ak/bk→Lak​/bk​→L