Mathlib Changelog
v4
Changelog
About
Github
Theorem
LinearMap.tendsto_birkhoffAverage_of_ker_subset_closure
Modification history
2023-09-09 17:26
Mathlib/Analysis/InnerProductSpace/MeanErgodic.lean
feat: von Neumann Mean Ergodic Theorem (#6053)
Added
LinearMap.tendsto_birkhoffAverage_of_ker_subset_closure
View on Github →