Birkhoff ergodic theorem

Stream: maths

[Yury G. Kudryashov]

Is there a proof of the Birkhoff ergodic theorem that works (directly) for functions f : α → E, not f : α → ℝ?

[Yury G. Kudryashov]

I understand that we can prove it for f : α → ℝ, then go to f : α → E for a "nice" E (not sure about specific assumptions).

[Yury G. Kudryashov]

BTW, is it true for an infinite dimensional E?

[Sebastien Gouezel]

I only know proofs that go through ℝ, using the order structure and maximal inequalities. Once you have it for ℝ, you deduce it for an arbitrary Banach space (for ae strongly measurable functions), by approximating the function by a finite linear combination of characteristic functions. For each of these, the one-dimensional result applies, and taking the norm you can also estimate the error in the approximation using the one-dimensional result.

[Yury G. Kudryashov]

Thank you! I'll think about details tomorrow.

[Yury G. Kudryashov]

Is this implication written somewhere? I tried to fill in the details and failed.

[Sebastien Gouezel]

Maybe I was overly optimistic. Let me try to write down the details, in the ergodic case first for simplicity.

Let u : E -> F be integrable. It is approximated in L^1 by a simple function ∑ i, 1_{s_i} • a i, where a i are elements of F and s i are measurable sets. Say u = v + ∑ i, 1_{s_i} • a i where v has L^1 norm at most epsilon.

Then S_n u / n = S_n v / n + ∑ i, (S_n 1_{s_i})/n • a i. Almost everywhere, the latter sum converges (by Birkhoff applied to the real function 1_{s_i}), while the limsup of S_n v / n is bounded by epsilon (again by Birkhoff applied to the norm of v). It follows that S_n u / n oscillates asymptotically by at most epsilon.

Letting epsilon tend to zero along a countable sequence, one deduces that, almost surely, S_n u / n is a Cauchy sequence, therefore convergent. Its limit is an invariant function, therefore constant. As its integral is the integral of u, this constant is the integral of u.

[Sebastien Gouezel]

Consider now the slightly harder non-ergodic case. Then S_n ||v|| / n still converges almost surely, but its limit (the conditional expectation of ||v|| with respect to the invariant sigma-algebra) doesn't have to be small everywhere. However, it is bounded by epsilon in L^1, so it is smaller than epsilon^{1/2} outside of a set of small measure (at most epsilon^{1/2}). Moreover, the conditional expectation of u is close to ∑ i, E(1_{s_i} | I) • a i again outside a set of small measure. Taking epsilon_n = 2^{-n} and applying Borel-Cantelli, one obtains the almost sure convergence of S_n u / n to E(u | I).

[Yury G. Kudryashov]

I think that I missed the Borel-Cantelli step when I was trying to do that. Thank you!

[Sebastien Gouezel]

I realized that we didn't even have the strong law of large numbers for vector-valued observables, so I implemented it following the above proof sketch (but without the need for Borel-Cantelli as there are only constant limits), see #7218. It went pretty smoothly (although it highlighted some gaps in the library and some superfluous second-countability assumptions here and there, as always).

[Yury G. Kudryashov]

In the meantime, I'm busy with dull stuff like getting rid of docs#Metric.Bounded and migrating to docs#Bornology.IsBounded.

[Lua Viana Reis]

Hi, I now have a proof of the maximal inequality in a fork. With it, we can show that the set of f : α → E for which the Birkhoff averages converge pointwise is closed in L1.

Then, my plan is to rework the existing MeanErgodic.lean a bit to extract the proof that the coboundaries are L2-dense in the orthogonal complement of the invariant functions (which is inside a proof in there). For coboundaries and invariant functions the theorem is trivial, and the L1-closure of their sums is also the whole L1 because the L2 norm is stronger.

For the first part (showing it is closed), I think it would be very useful if Mathlib had some API around the following definition: for f : α → β, Preorder α and PseudoMetricSpace β,

$$\Omega(f) = \limsup_{(a, b) \to \infty} d(f(a), f(b))$$

(which is like the "oscillation" limsup a_n - liminf a_n that is commonly used to show convergence for sequences of real numbers). Then CauchySeq f ↔ Ω f = 0.

This is particularly useful because to show it's closed, I would use the bound

$$\Omega(A_n f) \le \Omega(A_n (f - g)) + \Omega(A_n g).$$

If pointwise convergence is true for $g$, then $\Omega(A_ng) = 0$, and the maximal theorem says

$$\mu\big(\exists n, A_n \|f - g\| > \alpha\big) \le \frac{1}{\alpha} \|f-g\|_1.$$

Fixing $\alpha$ and letting $\|f-g\|_1 \to 0$, we have

$$\Omega(A_n f) \le \alpha$$

almost everywhere, so now we let $\alpha = 1/k \to 0$. I could not find a convenient way to do this sort of manipulation using the existing API, because not until the last step we show the sequence $A_nf$ is pointwise Cauchy (so the CauchySeq predicate does not help), and nowhere in the proof we mention the actual limit of the averages (so I cannot use Tendsto). But perhaps there is a better approach for this step without introducing $\Omega$. :slight_smile: