Theorem birkhoffAverage_apply_sub_birkhoffAverage

Modification history

2025-08-17 06:46
Mathlib/Dynamics/BirkhoffSum/Average.lean
feat(Dynamics/BirkhoffSum/Average): add lemma `birkhoffAverage_of_invariant` (#26842) …
Modified birkhoffAverage_apply_sub_birkhoffAverageView on Github →
2023-09-09 17:26
Mathlib/Dynamics/BirkhoffSum/Average.lean
feat: von Neumann Mean Ergodic Theorem (#6053)
Modified birkhoffAverage_apply_sub_birkhoffAverageView on Github →
2023-08-10 19:52
Mathlib/Dynamics/BirkhoffSum/Average.lean
chore: banish `Type _` and `Sort _` (#6499) …
Modified birkhoffAverage_apply_sub_birkhoffAverageView on Github →
2023-07-25 20:35
Mathlib/Dynamics/BirkhoffSum/Average.lean
feat(Dynamics/Birkhoff): define Birkhoff sum and Birkhoff average (#6131)
Added birkhoffAverage_apply_sub_birkhoffAverageView on Github →