Existence of Banach limits: Translation invariance A positive functional $\Phi$ on $\ell^{\infty}$ is said to be a Banach limit if $\Phi(1,1,1,\ldots)=1$ and $\Phi\circ L=\Phi$ where $L$ is the left shift operator on $\ell^{\infty}$.

Show that there exists a Banach limit.

My attempt: Consider the functionals $p: (x_n)\mapsto \limsup x_n$ on $\ell^{\infty}$ and $f:(x_n)\mapsto \lim x_n$ on $c$ (the space of convergent sequences). Then $f$ is linear, $p$ is sublinear, and $f\le p$ on $c$.
Therefore  by Hahn Banach theorem, there exists a functional $\Phi$ on $\ell^{\infty}$ such that $\Phi=f$ on $c$ and $\Phi\le p$ on $\ell^{\infty}$. As $f$ is positive, so is $\Phi$. Moreover, $\Phi(1,1,1,\ldots)=f(1,1,1,\ldots)=1$.
My question: How to show that $\Phi\circ L=\Phi$?
I observed the following: $f\circ L=f=p$ on $c$ and $p\circ L=p$ on $\ell^{\infty}$ but don't know if it's useful.
 A: You can't. It is not true in general that $\Phi \circ L = \Phi$. Let $u$ be the sequence $(1,-1,1,-1,\ldots)$ which is in $\ell^\infty$ but not in $c$.  We can extend $f$ from $c$ to
$\text{span}(u, c)$ by taking the value at $u$ to be anything in $[-1,1]$, and still have the extension be bounded by $p$.  Then extend again to $\ell^\infty$ using Hahn-Banach.
But since $L(u) = -u$, this $\Phi$ satisfies $\Phi \circ L (u) = \Phi(u)$ only if $\Phi(u) = 0$.
A: Let $V$ be the subspace of $\ell^\infty $ consisting of sequences $x$ for which the limit $$f(x):=\lim_n{x_1+x_2+\ldots +x_n\over n}$$ exists. Then $c\subset V$ and $f(x)=\lim_nx_n, $ for $x\in c.$ Since $$\left |{x_1+x_2+\ldots +x_n\over n}\right |\le \|x\|_\infty$$ we get $|f(x)|\le \|x\|_\infty.$ By the Hahn-Banach theorem there exists a linear functional $F:\ell^\infty \to \mathbb{C}$ such that $|F(x)|\le \|x\|_\infty$ and $F(x)=f(x)$ for $x\in V.$
Let $x\in \ell^\infty.$ Denote by $s(x)$  the shifted sequence $s(x)_n=x_{n+1}.$ Then $y:=x-s(x)\in V$ and $f(y)=0.$ Indeed $${y_1+y_2+\ldots +y_n\over n}={x_1-x_{n+1}\over n}\to 0$$ Hence $$F(x)-F(s(x))=F(x-s(x))=f(x-s(x))=0$$ Thus $F(s(x))=F(x)$ which gives the translation invariance property.
