Ergodic Theorem and Nonstandard Analysis Here is a quote from Lectures on Ergodic Theory by Halmos:

I cannot resist the temptation of
  concluding these comments with an
  alternative "proof" of the ergodic
  theorem. If $f$ is a complex valued
  function on the nonnegative integers,
  write $\int f(n)dn=\lim
> \frac{1}{n}\sum_{j=1}^nf(n)$ and whenever
  the limit exists call such
  functions integrable. If $T$ is a
  measure preserving transformation on a
  space $X$, then $$
> \int\int|f(T^nx)|dndx=\int\int|f(T^nx)|dxdn=\int\int|f(x)|dxdn=\int|f(x)|dx<\infty.
> $$ Hence, by "Fubini's theorem" (!),
  $f(T^nx)$ is an integrable function of
  its two arguments, and therefore, for
  almost every fixed $x$ it is an
  integrable function of $n$. Can any of
  this nonsense be made meaningful?

Can any of this nonsense be made meaningful using nonstandard analysis? I know that Kamae gave a short proof of the ergodic theorem using nonstandard analysis in A simple proof of the ergodic theorem using nonstandard analysis, Israel Journal of Mathematics, Vol. 42, No. 4, 1982. However, I have to say that I am not satisfied with his proof. It is tricky and not very illuminating, at least for me. Besides, it does not look anything like the so called proof proposed by Halmos. Actually, Kamae's idea can be made standard in a very straightforward manner. See for instance A simple proof of some ergodic theorems by Katznelson and Weiss in the same issue of the Israel Journal of Mathematics. By the way, Kamae's paper is 7 pages and Katznelson-Weiss paper is 6 pages.
To summarize, is there a not necessarily short but conceptually clear and illuminating proof of the ergodic theorem using nonstandard analysis, possibly based on the intuition of Halmos?
 A: I feel the answer is "no", at least while staying true to the spirit of Halmos's text.  Halmos's "proof", if valid, would imply something far stronger (and false), namely that $\lim_{N \to \infty} \frac{1}{N} \sum_{n=1}^N f(T_n x)$ converged for almost every x, where $T_1, T_2, \ldots$ are an arbitrary sequence of measure-preserving transformations.  This is not true even in the case when X is a two-element set.  So any proof of the ergodic theorem must somehow take advantage of the group law $T^n T^m = T^{n+m}$ in some non-trivial way.
That said, though, nonstandard analysis does certainly generate a Banach limit functional $\lambda: \ell^\infty({\bf N}) \to {\bf C}$ which one does induce something resembling an integral, namely the Cesaro-Banach functional
$f \mapsto \lambda( (\frac{1}{N} \sum_{n=1}^N f(n) )_{N \in {\bf N}} ).$
This does somewhat resemble an integration functional on the natural numbers, in that it is finitely additive and translation invariant.  But it is not countably additive, and tools such as Fubini's theorem do not directly apply to it; also, this functional makes sense even when the averages don't converge, so it doesn't seem like an obvious tool in order to demonstrate convergence.
A: There is a short proof in Katok's book. Introduction to the modern theory of dynamical systems [Book]
