LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-6-luna)

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.

Limit formula for linearly bounded superadditive sequences

Statement

Let $(a_{n})_{n \geq 0}$ be a real sequence with $a_{0} = 0$ , $a_{m + n} \geq a_{m} + a_{n}$ for all $m, n \geq 0$ , and $∣ a_{n} ∣ \leq C n$ for some finite constant $C$ . Then

$\lim_{n \to \infty} \frac{a_{n}}{n} = \sup_{k \geq 1} \frac{a_{k}}{k} .$

Facts & Assumptions

Given: The real sequence and superadditivity and linear boundedness assumptions in the Statement.

[A1]

$a_{m + n} \geq a_{m} + a_{n}$ for all nonnegative integers $m, n$ , and $∣ a_{n} ∣ \leq C n$ .

Proof

1.1givenA1algebra

Set $α : = \sup_{k \geq 1} a_{k} / k$ . The bound in [A1] makes $α$ finite, and the definition of supremum gives $a_{n} / n \leq α$ for every $n \geq 1$ . Hence ${lim sup}_{n \to \infty} a_{n} / n \leq α$ .

1.2givenA1algebrachoose

Fix $k \geq 1$ . For each $n$ , write $n = q k + r$ with integers $q \geq 0$ and $0 \leq r < k$ . Repeated use of superadditivity in [A1] gives $a_{n} \geq q a_{k} + a_{r}$ . The finitely many values $a_{0}, \dots, a_{k - 1}$ have a finite minimum $m_{k}$ , so $a_{n} / n \geq (q / n) a_{k} + m_{k} / n$ . As $n \to \infty$ , $q / n \to 1 / k$ and $m_{k} / n \to 0$ , yielding ${lim inf}_{n \to \infty} a_{n} / n \geq a_{k} / k$ .

2.1step 1.1step 1.2algebra∎

Since step 1.2 holds for every $k \geq 1$ , taking the supremum gives ${lim inf}_{n \to \infty} a_{n} / n \geq α$ . Combining with step 1.1 proves the asserted limit and its value.

Used by

Dependency tree · 0 levels

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

Sources

Igor Devetak, The private classical capacity and quantum capacity of a quantum channel, Appendix A discussion of regularization limits (standard reference, not scraped)
John Watrous, The Theory of Quantum Information, Appendix A, regularization of channel capacities (standard reference, not scraped)