Commit 2023-07-25 20:35 cf605654

View on Github →

feat(Dynamics/Birkhoff): define Birkhoff sum and Birkhoff average (#6131)

Estimated changes

added def birkhoffAverage
added theorem birkhoffAverage_one'
added theorem birkhoffAverage_one
added theorem birkhoffAverage_zero'
added theorem birkhoffAverage_zero
added theorem map_birkhoffAverage
added def birkhoffSum
added theorem birkhoffSum_add
added theorem birkhoffSum_one'
added theorem birkhoffSum_one
added theorem birkhoffSum_succ'
added theorem birkhoffSum_succ
added theorem birkhoffSum_zero'
added theorem birkhoffSum_zero
added theorem map_birkhoffSum