time averages for ergodic theorems?

Stream: maths

[Yury G. Kudryashov]

In #6053, I prove von Neumann Mean Ergodic Theorem (for an isometric linear operator in a Hilbert space). Neither the statement, nor the proof look like they should. I think that a more readable way to introduce

def timeAverage (f : α → α) (g : α → E) (N : ℕ) (x : α) : E :=
  (N : ??)¯¹ • ∑ n in range N, g (f^[n] x)

then reformulate the theorem in terms of this function. However, it is not clear which field we should cast N to. Also, should we allow N = 0 or use N + 1 in the definition so that f x = x → ∀ N, timeAverage f g N x = g x?

[Yury G. Kudryashov]

(I know that the proof is not readable and I should move many steps to lemmas before making it awaiting-review)

[Yury G. Kudryashov]

@Sebastien Gouezel @Oliver Nash :up:

[Sebastien Gouezel]

I would define birkhoffSum f g N x = ∑ n in range N, g (f^[n] x), and then reformulate your theorem with (N : 𝕜)⁻¹ • birkhoffSum f g N x. This is already more readable, and avoids the casting issue. And also the N = 0 issue: in your case, you always have birkhoffSum f g N x = N • g x.