OperatorMeanErgodic.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.Nonhyperlinear.Diffuseness.cesaro_on_closedRange line 11
lemma OAI.Nonhyperlinear.Diffuseness.cesaro_fixed line 32
theorem OAI.Nonhyperlinear.Diffuseness.cesaro_tendsto_fixedProjection line 45
Source documentation
The Hilbert mean ergodic theorem for a selfadjoint contraction, proved using telescoping on the dense range and the fixed-space orthogonal projection.
```
theorem cesaro_tendsto_fixedProjection (S : H →L[ℂ] H)
    (hS : ‖S‖≤1) (hstar : star S=S) (x : H) :
    Tendsto (fun n=>cesaro S n x) atTop (𝓝 ((1-S).ker.starProjection x)) := by
…
```
Mentions: OAI.Nonhyperlinear.Diffuseness.cesaro