birkhoffAverage_apply_sub_birkhoffAverage

theorem birkhoffAverage_apply_sub_birkhoffAverage : ∀ {α : Type u_1} {M : Type u_2} (R : Type u_3) [inst : DivisionRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (f : α → α) (g : α → M) (n : ℕ) (x : α), birkhoffAverage R f g n (f x) - birkhoffAverage R f g n x = (↑n)⁻¹ • (g (f^[n] x) - g x)

The theorem `birkhoffAverage_apply_sub_birkhoffAverage` states that for any division ring `R`, additive commutative group `M`, functions `f` mapping from a type `α` to `α` and `g` mapping from `α` to `M`, natural number `n`, and value `x` of type `α`, the difference between the Birkhoff averages of `f x` and `x` is equal to the inverse of `n` (as an element of `R`) multiplied by the difference between `g` applied to `f` iterated `n` times at `x` and `g x`. This can be interpreted as the Birkhoff average being "almost invariant" under `f`.

More concisely: For any division ring R, additive commutative group M, functions f and g, natural number n, and value x, the difference between the Birkhoff averages of f(x) and x is equal to (1/n) * (g ∘ f^n (x) - g(x)).