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?