CorollaryStatement: 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, $0 / 0$ form: if $b_{k}$ is strictly decreasing to $0$ , $a_{k} \to 0$ , and the difference quotient converges, then $a_{k} / b_{k}$ converges to the same value

Statement

Let $(a_{k})$ and $(b_{k})$ be sequences of reals (Sequences of reals: bounded, eventually, frequently, tails, subsequences) with $(b_{k})$ strictly decreasing (Nondecreasing, increasing, nonincreasing, decreasing, monotone, and eventually monotone sequences), $\lim_{k} b_{k} = 0$ and $\lim_{k} a_{k} = 0$ . 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$ , exactly as in 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$ . Suppose $(d_{k})$ converges.

Then $b_{k} > 0$ for every $k$ , so $(a_{k} / b_{k})$ is a sequence of reals; that sequence converges, and

$\lim_{k} \frac{a_{k}}{b_{k}} = \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. 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 decreasing, $\lim_{k} b_{k} = 0$ , $\lim_{k} a_{k} = 0$ , and 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 and strict decrease: $b_{j} > b_{k}$ for $j < k$ , so $b_{k} - b_{k + 1} > 0$ (Sequences of reals: bounded, eventually, frequently, tails, subsequences, Nondecreasing, increasing, nonincreasing, decreasing, monotone, and eventually monotone sequences).

[L2]

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); a constant sequence converges to its value; limits are unique (A sequence has at most one limit).

[L3]

Limits preserve non-strict inequalities, hypotheses needed only eventually (Limits preserve non-strict inequalities).

[L4]

Algebra of limits for sums, differences and scalar multiples (Algebra of limits: sums, scalar multiples, products and quotients).

[L5]

Finite sums (Finite sums and finite products, by recursion) and their laws: telescoping, splitting, additivity, scaling and monotonicity in the terms (Laws of finite sums and finite products).

[L6]

Triangle inequality for finite sums (Triangle inequality for finite sums); $∣ u v ∣ = ∣ u ∣ ∣ v ∣$ , $∣ u ∣ = u$ for $u \geq 0$ , and $∣ u ∣ \leq c$ exactly when $- c \leq u \leq c$ (Basic properties of the absolute value).

[L7]

Order arithmetic: $a > 0$ gives $a^{- 1} > 0$ (Inverses of positives are positive, and reciprocation reverses order); for $c > 0$ , $a \leq b$ if and only if $a c \leq 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); of two indices one is the larger ( $\leq$ is a linear order on $N$ ). In each clause above, Sign rules for products and monotonicity of multiplication and Order is preserved by adding a constant and by adding inequalities state the STRICT forms and only those; the nonstrict forms used below are those together with the equality cases, which trichotomy settles, the order being total (Ordered field).

Proof

technique · direct

1.1

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

L1L7

1.2

$b_{m} > 0$ for every $m$ : for all $k \geq m + 1$ one has $b_{k} \leq b_{m + 1}$ , so comparing $(b_{k})$ with the constant sequence $b_{m + 1}$ gives $0 = \lim_{k} b_{k} \leq b_{m + 1}$ , and $b_{m + 1} < b_{m}$ then gives $b_{m} > 0$ .

L1L2L3

1.3

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

L2L7choose

2.1

For all $n > m \geq K$ : telescoping gives $a_{m} - a_{n} = \sum_{k = m}^{n - 1} (a_{k} - a_{k + 1}) = \sum_{k = m}^{n - 1} d_{k} (b_{k} - b_{k + 1})$ and $b_{m} - b_{n} = \sum_{k = m}^{n - 1} (b_{k} - b_{k + 1})$ , so $∣ a_{m} - a_{n} - L (b_{m} - b_{n}) ∣ \leq \sum_{k = m}^{n - 1} ∣ d_{k} - L ∣ (b_{k} - b_{k + 1}) \leq (ε / 2) (b_{m} - b_{n})$ , that is $- (ε / 2) (b_{m} - b_{n}) \leq a_{m} - a_{n} - L (b_{m} - b_{n}) \leq (ε / 2) (b_{m} - b_{n})$ .

step 1.1step 1.3L5L6L7

3.1

Fix $m \geq K$ and let $n$ vary over the indices $> m$ : since $a_{n} \to 0$ and $b_{n} \to 0$ , the middle quantity converges in $n$ to $a_{m} - L b_{m}$ , the right-hand one to $(ε / 2) b_{m}$ and the left-hand one to $- (ε / 2) b_{m}$ ; the two eventual inequalities of step 2.1 therefore pass to the limit and give $- (ε / 2) b_{m} \leq a_{m} - L b_{m} \leq (ε / 2) b_{m}$ .

step 2.1L2L3L4

4.1

Since $b_{m} > 0$ , dividing by $b_{m}$ gives $∣ a_{m} / b_{m} - L ∣ \leq ε / 2 < ε$ for every $m \geq K$ .

step 1.2step 3.1L6L7

5.1

As $ε > 0$ was arbitrary, $(a_{k} / b_{k})$ converges to $L$ , so $\lim_{k} a_{k} / b_{k}$ exists and equals $L = \lim_{k} d_{k}$ .

step 4.1L2∎

Remarks

This is a companion of 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$ rather than a formal consequence of it, and the cor- prefix should be read that way. The two statements share hypotheses of the same shape and the same telescoping device, but neither is obtained by substituting data into the other: there the fixed head $a_{K} - L b_{K}$ is washed out because $b_{n}$ grows without bound, here the head is removed by letting the far end of the telescope go to $0$ . Nothing in the proof above cites the theorem.
Where the limit is taken matters. In step 3.1 the index $m$ is frozen and $n$ runs; the estimate of step 2.1 is uniform in $n$ for that fixed $m$ , which is why the passage to the limit is legitimate. Taking both indices to infinity at once would prove nothing.
The conclusion is non-strict at the level of $ε / 2$ and is turned into the strict inequality demanded by the definition of a limit only at the last division, where $ε / 2 < ε$ . That is the usual price of passing an inequality to a limit (Limits preserve non-strict inequalities): strictness is not preserved, so it has to be recovered by halving.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

50 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)
J. Lebl, Basic Analysis I, §2.2 and §2.3 (standard reference, not scraped)

Stolz-Cesaro, 0/00/0 form: if bkbk​ is strictly decreasing to 00, ak→0ak​→0, and the difference quotient converges, then ak/bkak​/bk​ converges to the same value