Exact source: MathlibAnnex/Analysis/InnerProductSpace/DecreasingProjection.lean
Pinned GitHub source · Raw UTF-8 source
Back to The atomic common range is one embedded GNS line · Back to The matching GNS fiber retains exactly its cyclic line · Back to An inequivalent GNS fiber has no residual common range
1import Mathlib.Analysis.InnerProductSpace.Projection.Submodule2import MathlibAnnex.Analysis.InnerProductSpace.StrongOperator34/-!5# Strong limits of decreasing orthogonal projections67The result is stated for an arbitrary directed preorder. For a decreasing8sequence it identifies the strong limit with the orthogonal projection onto9the common fixed subspace, represented by the infimum of the ranges.10-/1112set_option autoImplicit false1314open Filter Topology1516namespace Submodule1718variable {𝕜 E ι : Type*}19variable [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E]20variable [CompleteSpace E] [Preorder ι]2122private theorem closure_iSup_orthogonal (U : ι → Submodule 𝕜 E)23 [∀ i, (U i).HasOrthogonalProjection] :24 (⨆ i, (U i)ᗮ).topologicalClosure = (⨅ i, U i)ᗮ := by25 rw [← orthogonal_orthogonal_eq_closure, ← iInf_orthogonal]26 simp only [orthogonal_orthogonal]2728/-- Orthogonal projections onto an antitone family of complete subspaces29converge strongly to the projection onto their intersection. -/30theorem tendsto_starProjection_iInf (U : ι → Submodule 𝕜 E)31 [∀ i, (U i).HasOrthogonalProjection]32 [(⨅ i, U i).HasOrthogonalProjection] (hU : Antitone U) (x : E) :33 Tendsto (fun i ↦ (U i).starProjection x) atTop34 (𝓝 ((⨅ i, U i).starProjection x)) := by35 let V : ι → Submodule 𝕜 E := fun i ↦ (U i)ᗮ36 have hV : Monotone V := fun _ _ hij ↦ orthogonal_le (hU hij)37 have hlim := starProjection_tendsto_closure_iSup V hV x38 have hclosure : (⨆ i, V i).topologicalClosure = (⨅ i, U i)ᗮ :=39 closure_iSup_orthogonal U40 have hlim' : Tendsto (fun i ↦ (V i).starProjection x) atTop41 (𝓝 ((⨅ i, U i)ᗮ.starProjection x)) := by42 simpa only [hclosure] using hlim43 have hcomp : Tendsto (fun i ↦ x - (V i).starProjection x) atTop44 (𝓝 (x - (⨅ i, U i)ᗮ.starProjection x)) := by45 exact tendsto_const_nhds.sub hlim'46 simpa [V, starProjection_orthogonal] using hcomp4748/-- Operator-valued formulation of `tendsto_starProjection_iInf`. -/49theorem stronglyConverges_starProjection_iInf (U : ι → Submodule 𝕜 E)50 [∀ i, (U i).HasOrthogonalProjection]51 [(⨅ i, U i).HasOrthogonalProjection] (hU : Antitone U) :52 ContinuousLinearMap.StronglyConverges (fun i ↦ (U i).starProjection) atTop53 (⨅ i, U i).starProjection :=54 fun x ↦ tendsto_starProjection_iInf U hU x5556/-- The infimum of the ranges is exactly the common fixed-point subspace. -/57theorem mem_iInf_iff_starProjection_eq_self (U : ι → Submodule 𝕜 E)58 [∀ i, (U i).HasOrthogonalProjection] {x : E} :59 x ∈ ⨅ i, U i ↔ ∀ i, (U i).starProjection x = x := by60 simp only [mem_iInf, starProjection_eq_self_iff]6162end Submodule