Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-14
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 L:(N;R)R such that

L(1)=1,L=1,L(Sx)=L(x),

where (Sx)n=xn+1. Moreover L(x)=limnxn whenever the ordinary limit exists.

Facts & Assumptions

[A1]

The Axiom of Choice holds (The Axiom of Choice).

[L1]

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).

[L3]

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

technique · direct

Given: The objects and hypotheses in the Statement.

1.1

For x define [given, L2, L3] p(x)=lim supN1N+1n=0Nxn. This is finite because x is bounded. Linearity of finite averages, positive homogeneity of limsup, and [L2] show that p is sublinear in the sense of [L3].

L2L3definition
2.1

Let c be the subspace of ordinarily convergent sequences and let [given, L1, A1, step 1.1] f(x)=limnxn on c. Cesaro means preserve an ordinary limit, so f(x)=p(x) on c; in particular fp. Apply [L1]. The exact non-finite choice use is [A1] in Hahn--Banach, producing a real-linear extension L with L(x)p(x) for every x.

A1L1step 1.1Cesaro convergence
3.1

If xn0, then p(x)0, hence [given, step 2.1] L(x)=L(x)p(x)0; thus L is positive. Since 1c, L(1)=1. Positivity applied to x1±x gives L(x)x, while L(1)=1 gives the reverse norm bound. Therefore L=1.

step 2.1positivity
4.1

The Cesaro average of xSx equals [given, step 2.1, step 1.1, step 3.1] (x0xN+1)/(N+1) and tends to zero; the same is true of Sxx. Therefore p(xSx)=p(Sxx)=0. Domination gives L(xSx)0 and L(xSx)=L(Sxx)0, so L(xSx)=0 and L(Sx)=L(x). On the original subspace c, step 2.1 already says that L extends the ordinary limit.

step 1.1step 2.1telescoping

Depends on

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