English
For a LinearPMap with complete space E, the adjoint gives a relation that remains linear; this is a structural fact about adjoints.
Русский
Для линейного частичного отображения с полным пространством E сопряжение обеспечивает линейное отношение; это структурное свойство сопряжения.
LaTeX
$$∀ A, A† is well-defined and linear on its domain$$
Lean4
/-- **Von Neumann Mean Ergodic Theorem** for an operator in a Hilbert space.
For a contracting continuous linear self-map `f : E →L[𝕜] E` of a Hilbert space, `‖f‖ ≤ 1`,
the Birkhoff averages
```
birkhoffAverage 𝕜 f id N x = (N : 𝕜)⁻¹ • ∑ n ∈ Finset.range N, f^[n] x
```
converge to the orthogonal projection of `x` to the subspace of fixed points of `f`. -/
theorem tendsto_birkhoffAverage_orthogonalProjection (f : E →L[𝕜] E) (hf : ‖f‖ ≤ 1) (x : E) :
Tendsto (birkhoffAverage 𝕜 f _root_.id · x) atTop (𝓝 <| (LinearMap.eqLocus f 1).orthogonalProjection x) := by
/- Due to the previous theorem, it suffices to verify
that the range of `f - 1` is dense in the orthogonal complement
to the submodule of fixed points of `f`. -/
apply (f : E →ₗ[𝕜] E).tendsto_birkhoffAverage_of_ker_subset_closure (f.lipschitz.weaken hf)
· exact (LinearMap.eqLocus f 1).orthogonalProjection_mem_subspace_eq_self
· clear x
rw [Submodule.ker_orthogonalProjection, ← Submodule.topologicalClosure_coe, SetLike.coe_subset_coe, ←
Submodule.orthogonal_orthogonal_eq_closure]
/- To verify this, we verify `‖f x‖ ≤ ‖x‖` (because `‖f‖ ≤ 1`) and `⟪f x, x⟫ = ‖x‖²`. -/
refine Submodule.orthogonal_le fun x hx ↦ eq_of_norm_le_re_inner_eq_norm_sq (𝕜 := 𝕜) ?_ ?_
· simpa using f.le_of_opNorm_le hf x
· have : ∀ y, ⟪f y, x⟫ = ⟪y, x⟫ := by simpa [Submodule.mem_orthogonal, inner_sub_left, sub_eq_zero] using hx
simp [this, ← norm_sq_eq_re_inner]
