birkhoffSum_apply_sub_birkhoffSum

theorem birkhoffSum_apply_sub_birkhoffSum : ∀ {α : Type u_1} {G : Type u_2} [inst : AddCommGroup G] (f : α → α) (g : α → G) (n : ℕ) (x : α), birkhoffSum f g n (f x) - birkhoffSum f g n x = g (f^[n] x) - g x

The theorem `birkhoffSum_apply_sub_birkhoffSum` states that for any function `f` mapping a type `α` to itself, a function `g` mapping `α` to a type `G` under an addition commutative group, a natural number `n`, and a value `x` of type `α`, the difference between the Birkhoff sum of `f` and `g` over the first `n` points of the orbit of `f(x)` and the Birkhoff sum of `f` and `g` over the first `n` points of the orbit of `x` is equal to the difference between the `n`th point in the orbit of `x` under `f` and `x` itself. In mathematical terms, we have $$ B_n(f, g, f(x)) - B_n(f, g, x) = g(f^n(x)) - g(x) $$ where $B_n(f, g, x)$ denotes the Birkhoff sum of `f` and `g` over the first `n` points of the orbit of `x`. This property shows a certain level of "almost invariance" of the Birkhoff sum under the action of `f`.

More concisely: The difference between the Birkhoff sums of a self-mapping function `f` and a group homomorphism `g` over the first `n` points of the orbit of `x` is equal to `g(f^n(x)) - g(x)`.