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.
Existence of a shift-invariant mean on bounded sequences
Statement
Assume the Axiom of Choice. There exists a positive real-linear functional such that
where . Moreover whenever the ordinary limit exists.
Facts & Assumptions
The Axiom of Choice holds (The Axiom of Choice).
Under AC, a real linear functional dominated by a sublinear functional on a subspace extends, with the domination preserved (Hahn-Banach dominated extension theorem for real vector spaces).
Cesaro means are finite averages (The Cesaro means and -summability), and limsup is subadditive ( whenever the right-hand side is defined in , and dually for ).
A sublinear functional is positively homogeneous and subadditive (A sublinear functional on a real vector space); bounded real sequences form real (The sequence spaces c_0 and ell-infinity).
Proof
Given: The objects and hypotheses in the Statement.
For define [given, L2, L3] . This is finite because is bounded. Linearity of finite averages, positive homogeneity of limsup, and [L2] show that is sublinear in the sense of [L3].
Let be the subspace of ordinarily convergent sequences and let [given, L1, A1, step 1.1] on . Cesaro means preserve an ordinary limit, so on ; in particular . Apply [L1]. The exact non-finite choice use is [A1] in Hahn--Banach, producing a real-linear extension with for every .
If , then , hence [given, step 2.1] ; thus is positive. Since , . Positivity applied to gives , while gives the reverse norm bound. Therefore .
The Cesaro average of equals [given, step 2.1, step 1.1, step 3.1] and tends to zero; the same is true of . Therefore . Domination gives and , so and . On the original subspace , step 2.1 already says that extends the ordinary limit.
Depends on
- The Axiom of Choice
- Hahn-Banach dominated extension theorem for real vector spaces
- The sequence spaces c_0 and ell-infinity
- The Cesaro means $\sigma_n = (x_0 + \dots + x_n)/(n+1)$ and $(C,1)$-summability
- A sublinear functional on a real vector space
- Limit superior and limit inferior of a real sequence as $\inf_n \sup_{k \ge n} x_k$ and $\sup_n \inf_{k \ge n} x_k$ in $\overline{\mathbb{R}}$
- $\limsup(x_k + y_k) \le \limsup x_k + \limsup y_k$ whenever the right-hand side is defined in $\overline{\mathbb{R}}$, and dually for $\liminf$
Used by
Dependency tree · two levels
39 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
- Gerald Teschl, Topics in Real and Functional Analysis, Problem 4.20 (standard reference, not scraped)