Exact source: MathlibAnnex/Analysis/InnerProductSpace/DecreasingProjection.lean, lines 30–46.
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.Submodule 2import MathlibAnnex.Analysis.InnerProductSpace.StrongOperator 3 4/-! 5# Strong limits of decreasing orthogonal projections 6 7The result is stated for an arbitrary directed preorder. For a decreasing 8sequence it identifies the strong limit with the orthogonal projection onto 9the common fixed subspace, represented by the infimum of the ranges. 10-/ 11 12set_option autoImplicit false 13 14open Filter Topology 15 16namespace Submodule 17 18variable {𝕜 E ι : Type*} 19variable [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] 20variable [CompleteSpace E] [Preorder ι] 21 22private theorem closure_iSup_orthogonal (U : ι → Submodule 𝕜 E) 23 [∀ i, (U i).HasOrthogonalProjection] : 24 (⨆ i, (U i)ᗮ).topologicalClosure = (⨅ i, U i)ᗮ := by 25 rw [← orthogonal_orthogonal_eq_closure, ← iInf_orthogonal] 26 simp only [orthogonal_orthogonal] 27 28/-- Orthogonal projections onto an antitone family of complete subspaces 29converge 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) atTop 34 (𝓝 ((⨅ i, U i).starProjection x)) := by 35 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 x 38 have hclosure : (⨆ i, V i).topologicalClosure = (⨅ i, U i)ᗮ := 39 closure_iSup_orthogonal U 40 have hlim' : Tendsto (fun i ↦ (V i).starProjection x) atTop 41 (𝓝 ((⨅ i, U i)ᗮ.starProjection x)) := by 42 simpa only [hclosure] using hlim 43 have hcomp : Tendsto (fun i ↦ x - (V i).starProjection x) atTop 44 (𝓝 (x - (⨅ i, U i)ᗮ.starProjection x)) := by 45 exact tendsto_const_nhds.sub hlim' 46 simpa [V, starProjection_orthogonal] using hcomp 47 48/-- 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) atTop 53 (⨅ i, U i).starProjection := 54 fun x ↦ tendsto_starProjection_iInf U hU x 55 56/-- 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 := by 60 simp only [mem_iInf, starProjection_eq_self_iff] 61 62end Submodule