Commit 2025-08-17 06:46 c5fbdc30

feat(Dynamics/BirkhoffSum/Average): add lemma birkhoffAverage_of_invariant (#26842) If a function g is invariant under a function f (i.e., g ∘ f = g), then the Birkhoff average of g over f for n iterations is equal to g. Requires that n ≠ 0.

• depends on: #26810