LemmaStatement: Literature-sourcedProof: AI-generatedPipeline-generated

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.

Almost-additive sequences have a normalized limit

Statement

Let $(a_{n})_{n \geq 1}$ be a real sequence for which there is a finite constant $K$ with $∣ a_{n} ∣ \leq K n$ for every $n \geq 1$ . Suppose there is a finite constant $C \geq 0$ such that $∣ a_{m + n} - a_{m} - a_{n} ∣ \leq C$ for all positive integers $m, n$ . Then $a_{n} / n$ has a finite limit as $n \to \infty$ .

Statement references

Formal almost-additive result: Subsection “Almost additive sequences,” lemma almost_additive_converges.

Textbook Fekete proof: §5.1, Theorem 5.1.

Independent real-analysis treatment: Appendix B.1.3, Lemma B.5.

Facts & Assumptions

Given: The linear bound and the almost-additivity inequality in the Statement.

Proof

1.1givenalgebra

Set $b_{n} = a_{n} + C$ and $c_{n} = a_{n} - C$ . The upper half of the assumed inequality gives $a_{m + n} \leq a_{m} + a_{n} + C$ , hence $b_{m + n} \leq b_{m} + b_{n}$ . The lower half gives $a_{m + n} \geq a_{m} + a_{n} - C$ , hence $c_{m + n} \geq c_{m} + c_{n}$ . Also $∣ b_{n} ∣, ∣ c_{n} ∣ \leq K n + C$ , so both sequences are bounded linearly.

2.1step 1.1algebra

For a linearly bounded subadditive sequence $b$ , fix $k \geq 1$ and write $n = q k + r$ with $0 \leq r < k$ . Iterating subadditivity, with $b_{0} = 0$ for the remainder case, gives $b_{n} \leq q b_{k} + b_{r}$ . The finitely many possible remainder values have a finite maximum $B_{k}$ , so $b_{n} / n \leq q b_{k} / n + B_{k} / n$ and therefore ${lim sup}_{n} b_{n} / n \leq b_{k} / k$ . Since this holds for every $k$ and ${lim inf}_{n} b_{n} / n \geq \inf_{k} b_{k} / k$ , the limit $b_{n} / n$ exists and is finite. Applying the same argument to $- c_{n}$ proves that $c_{n} / n$ has a finite limit.

3.1step 1.1step 2.1algebra∎

Since $b_{n} / n - c_{n} / n = 2 C / n \to 0$ and $c_{n} / n \leq a_{n} / n \leq b_{n} / n$ , the two limits from step 2.1 coincide and force $a_{n} / n$ to that same finite limit.

Used by

Communicating MDPs have a common optimal average reward Theorem

Dependency tree · 0 levels

Nothing. This result depends on no other item in the library.

Sources

Sébastien Gouëzel, Theory Fekete, Archive of Formal Proofs, lemma almost_additive_converges (standard reference, not scraped)
Wojciech Szpankowski, Average Case Analysis of Algorithms on Sequences (standard reference, not scraped)
Sacha Friedli and Yvan Velenik, Statistical Mechanics of Lattice Systems: A Concrete Mathematical Introduction (standard reference, not scraped)