Theorem ContinuousLinearMap.tendsto_birkhoffAverage_orthogonalProjection

Modification history

2023-09-09 17:26
Mathlib/Analysis/InnerProductSpace/MeanErgodic.lean
feat: von Neumann Mean Ergodic Theorem (#6053)
Added ContinuousLinearMap.tendsto_birkhoffAverage_orthogonalProjectionView on Github →