Shift domination criterion for a Banach limit (source code)

= Shift domination criterion for a Banach limit
{title2=$q\leq\limsup,\quad q(x-Sx)\leq0$}

Suppose $q$ is a <sublinear functional> on the bounded real sequences, dominated by the <limit superior> and nonpositive on every shift difference $x-Sx$. The <Hahn-Banach theorem> then yields a <Banach limit>. Indeed $0\leq q(x)+q(-x)$ implies $q(x)\geq-q(-x)\geq\liminf x_n$, so $q$ agrees with the ordinary limit on convergent sequences. Extend this linear limit functional by Hahn-Banach to a linear $\psi\leq q$. Domination on $x-Sx$ and on its negative forces $\psi(x)=\psi(Sx)$. The two-sided limit bounds give positivity, <norm> one and agreement with ordinary limits. In finite-shift averaging constructions, the needed bound on shift differences follows by telescoping consecutive averages to $(x_{n+1}-x_{n+k+1})/k$.