Commit 2023-09-09 17:26 0948c002

View on Github →

feat: von Neumann Mean Ergodic Theorem (#6053)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/InnerProductSpace/Basic.lean

added theorem eq_of_norm_le_re_inner_eq_norm_sq

Created Mathlib/Analysis/InnerProductSpace/MeanErgodic.lean

added theorem ContinuousLinearMap.tendsto_birkhoffAverage_orthogonalProjection

added theorem LinearMap.tendsto_birkhoffAverage_of_ker_subset_closure

Modified Mathlib/Dynamics/BirkhoffSum/Average.lean

modified theorem birkhoffAverage_apply_sub_birkhoffAverage

Created Mathlib/Dynamics/BirkhoffSum/NormedSpace.lean

added theorem Function.IsFixedPt.tendsto_birkhoffAverage

added theorem dist_birkhoffAverage_apply_birkhoffAverage

added theorem dist_birkhoffAverage_birkhoffAverage

added theorem dist_birkhoffAverage_birkhoffAverage_le

added theorem dist_birkhoffSum_apply_birkhoffSum

added theorem dist_birkhoffSum_birkhoffSum_le

added theorem isClosed_setOf_tendsto_birkhoffAverage

added theorem tendsto_birkhoffAverage_apply_sub_birkhoffAverage'

added theorem tendsto_birkhoffAverage_apply_sub_birkhoffAverage

added theorem uniformEquicontinuous_birkhoffAverage