Exact source: MathlibAnnex/Analysis/CStarAlgebra/Representation/ShellReconstruction.lean, lines 136–253.
Back to Reconstructing a represented unitary from its shells and residual corner
1import Mathlib.Analysis.CStarAlgebra.ContinuousLinearMap 2import MathlibAnnex.Analysis.CStarAlgebra.Representation.Basic 3import MathlibAnnex.Analysis.InnerProductSpace.ProjectionLimit 4import MathlibAnnex.Analysis.InnerProductSpace.ProjectionShell 5import MathlibAnnex.Analysis.InnerProductSpace.UnitaryCompletion 6 7/-! 8# Rebuilding shell strong sums in an arbitrary representation 9 10Only algebraic source identities are transported through the representation. 11The strong limits are then reconstructed in the target Hilbert space by the 12orthogonal-shell theorem; no representation is claimed to preserve a strong 13operator limit formed elsewhere. 14-/ 15 16set_option autoImplicit false 17 18open Filter Topology 19open scoped InnerProduct 20 21namespace MathlibAnnex.Analysis.CStarAlgebra 22 23universe u v 24 25variable {A : Type u} [CStarAlgebra A] 26variable {H : Type v} 27variable [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] 28 29/-- Star projections remain star projections under a unital star-algebra 30homomorphism. -/ 31theorem IsStarProjection.map_representation 32 (pi : Representation A H) {p : A} (hp : IsStarProjection p) : 33 IsStarProjection (pi p) := by 34 constructor 35 · rw [isIdempotentElem_iff, ← map_mul, hp.isIdempotentElem.eq] 36 · rw [isSelfAdjoint_iff, ← map_star, hp.isSelfAdjoint.star_eq] 37 38/-- Algebraic decreasing projection flags and exact shell supports rebuild 39both strong shell sums and their limiting products in every represented 40Hilbert space. -/ 41theorem exists_represented_strongSums_of_sourceShells 42 (pi : Representation A H) 43 (p q w : ℕ → A) 44 (hp : ∀ n, IsStarProjection (p n)) 45 (hq : ∀ n, IsStarProjection (q n)) 46 (hp0 : p 0 = 1) (hq0 : q 0 = 1) 47 (hp_le : ∀ ⦃m n : ℕ⦄, m ≤ n → p m * p n = p n) 48 (hq_le : ∀ ⦃m n : ℕ⦄, m ≤ n → q m * q n = q n) 49 (hInitial : ∀ n, star (w n) * w n = p n - p (n + 1)) 50 (hFinal : ∀ n, w n * star (w n) = q n - q (n + 1)) : 51 let U : ℕ → Submodule ℂ H := fun n ↦ (pi (p n)).range 52 let V : ℕ → Submodule ℂ H := fun n ↦ (pi (q n)).range 53 ∃ S T PU PV : H →L[ℂ] H, 54 ContinuousLinearMap.StronglyConverges 55 (ContinuousLinearMap.partialSum (fun n ↦ pi (w n))) atTop S ∧ 56 ContinuousLinearMap.StronglyConverges 57 (ContinuousLinearMap.partialSum (fun n ↦ (pi (w n))†)) atTop T ∧ 58 T = S† ∧ 59 IsStarProjection PU ∧ PU.range = ⨅ n, U n ∧ 60 IsStarProjection PV ∧ PV.range = ⨅ n, V n ∧ 61 (S†).comp S = 1 - PU ∧ 62 S.comp (S†) = 1 - PV := by 63 dsimp only 64 let U : ℕ → Submodule ℂ H := fun n ↦ (pi (p n)).range 65 let V : ℕ → Submodule ℂ H := fun n ↦ (pi (q n)).range 66 have hpPi (n : ℕ) : IsStarProjection (pi (p n)) := 67 IsStarProjection.map_representation pi (hp n) 68 have hqPi (n : ℕ) : IsStarProjection (pi (q n)) := 69 IsStarProjection.map_representation pi (hq n) 70 have hUdata (n : ℕ) : ∃ (_ : (U n).HasOrthogonalProjection), 71 pi (p n) = (U n).starProjection := by 72 simpa [U] using 73 (isStarProjection_iff_eq_starProjection_range.mp (hpPi n)) 74 have hVdata (n : ℕ) : ∃ (_ : (V n).HasOrthogonalProjection), 75 pi (q n) = (V n).starProjection := by 76 simpa [V] using 77 (isStarProjection_iff_eq_starProjection_range.mp (hqPi n)) 78 letI hUprojection (n : ℕ) : (U n).HasOrthogonalProjection := (hUdata n).choose 79 letI hVprojection (n : ℕ) : (V n).HasOrthogonalProjection := (hVdata n).choose 80 have hUproj (n : ℕ) : pi (p n) = (U n).starProjection := (hUdata n).choose_spec 81 have hVproj (n : ℕ) : pi (q n) = (V n).starProjection := (hVdata n).choose_spec 82 have hUclosed (n : ℕ) : IsClosed (U n : Set H) := by 83 exact ContinuousLinearMap.IsIdempotentElem.isClosed_range (hpPi n).isIdempotentElem 84 have hVclosed (n : ℕ) : IsClosed (V n : Set H) := by 85 exact ContinuousLinearMap.IsIdempotentElem.isClosed_range (hqPi n).isIdempotentElem 86 letI : IsClosed ((⨅ n, U n : Submodule ℂ H) : Set H) := by 87 simpa only [Submodule.coe_iInf] using isClosed_iInter hUclosed 88 letI : IsClosed ((⨅ n, V n : Submodule ℂ H) : Set H) := by 89 simpa only [Submodule.coe_iInf] using isClosed_iInter hVclosed 90 letI : CompleteSpace (⨅ n, U n : Submodule ℂ H) := inferInstance 91 letI : CompleteSpace (⨅ n, V n : Submodule ℂ H) := inferInstance 92 letI : (⨅ n, U n).HasOrthogonalProjection := inferInstance 93 letI : (⨅ n, V n).HasOrthogonalProjection := inferInstance 94 have hUanti : Antitone U := by 95 intro m n hmn 96 rintro x ⟨y, rfl⟩ 97 refine ⟨pi (p n) y, ?_⟩ 98 have heq : pi (p m) * pi (p n) = pi (p n) := by 99 rw [← map_mul, hp_le hmn] 100 exact congrArg (fun T : H →L[ℂ] H ↦ T y) heq 101 have hVanti : Antitone V := by 102 intro m n hmn 103 rintro x ⟨y, rfl⟩ 104 refine ⟨pi (q n) y, ?_⟩ 105 have heq : pi (q m) * pi (q n) = pi (q n) := by 106 rw [← map_mul, hq_le hmn] 107 exact congrArg (fun T : H →L[ℂ] H ↦ T y) heq 108 have hU0 : U 0 = ⊤ := by 109 rw [← Submodule.range_starProjection (U 0), ← hUproj, hp0, map_one] 110 exact LinearMap.range_eq_top.mpr fun x ↦ ⟨x, rfl⟩ 111 have hV0 : V 0 = ⊤ := by 112 rw [← Submodule.range_starProjection (V 0), ← hVproj, hq0, map_one] 113 exact LinearMap.range_eq_top.mpr fun x ↦ ⟨x, rfl⟩ 114 have hInitialPi (n : ℕ) : 115 ((pi (w n))†).comp (pi (w n)) = Submodule.projectionShell U n := by 116 change star (pi (w n)) * pi (w n) = _ 117 rw [← map_star, ← map_mul, hInitial, map_sub, hUproj, hUproj] 118 rfl 119 have hFinalPi (n : ℕ) : 120 (pi (w n)).comp ((pi (w n))†) = Submodule.projectionShell V n := by 121 change pi (w n) * star (pi (w n)) = _ 122 rw [← map_star, ← map_mul, hFinal, map_sub, hVproj, hVproj] 123 rfl 124 obtain ⟨S, T, hS, hT, _, _, hAdj, hProdU, hProdV⟩ := 125 ContinuousLinearMap.exists_strongSums_of_projectionShells 126 (fun n ↦ pi (w n)) U V hUanti hVanti hU0 hV0 hInitialPi hFinalPi 127 exact ⟨S, T, (⨅ n, U n).starProjection, (⨅ n, V n).starProjection, 128 hS, hT, hAdj, isStarProjection_starProjection, Submodule.range_starProjection _, 129 isStarProjection_starProjection, Submodule.range_starProjection _, hProdU, hProdV⟩ 130 131/-- A represented unitary satisfying the finite algebraic shell relations is 132reconstructed from strong sums formed afresh on the target Hilbert space. 133The complementary operator is supported exactly between the two represented 134limiting fixed spaces. In particular, this theorem never maps a strong limit 135through `pi`; only the finite source identities are mapped. -/ 136theorem exists_represented_unitaryCompletion_of_sourceShells 137 (pi : Representation A H) (e : H ≃ₗᵢ[ℂ] H) 138 (p q w : ℕ → A) 139 (hp : ∀ n, IsStarProjection (p n)) 140 (hq : ∀ n, IsStarProjection (q n)) 141 (hp0 : p 0 = 1) (hq0 : q 0 = 1) 142 (hp_le : ∀ ⦃m n : ℕ⦄, m ≤ n → p m * p n = p n) 143 (hq_le : ∀ ⦃m n : ℕ⦄, m ≤ n → q m * q n = q n) 144 (hInitial : ∀ n, star (w n) * w n = p n - p (n + 1)) 145 (hFinal : ∀ n, w n * star (w n) = q n - q (n + 1)) 146 (hUnitary : ∀ n, (e : H →L[ℂ] H).comp 147 (pi (p n - p (n + 1))) = pi (w n)) : 148 let U : ℕ → Submodule ℂ H := fun n ↦ (pi (p n)).range 149 let V : ℕ → Submodule ℂ H := fun n ↦ (pi (q n)).range 150 ∃ S T P Q R : H →L[ℂ] H, 151 ContinuousLinearMap.StronglyConverges 152 (ContinuousLinearMap.partialSum (fun n ↦ pi (w n))) atTop S ∧ 153 ContinuousLinearMap.StronglyConverges 154 (ContinuousLinearMap.partialSum (fun n ↦ (pi (w n))†)) atTop T ∧ 155 ‖S‖ ≤ 1 ∧ ‖T‖ ≤ 1 ∧ T = S† ∧ 156 IsStarProjection P ∧ P.range = ⨅ n, U n ∧ 157 IsStarProjection Q ∧ Q.range = ⨅ n, V n ∧ 158 (S†).comp S = 1 - P ∧ S.comp (S†) = 1 - Q ∧ 159 (e : H →L[ℂ] H) = S + R ∧ 160 R = (e : H →L[ℂ] H).comp P ∧ 161 (R†).comp R = P ∧ R.comp (R†) = Q ∧ 162 R = (Q.comp R).comp P ∧ 163 (∀ x, x ∈ ⨅ n, U n ↔ e x ∈ ⨅ n, V n) := by 164 dsimp only 165 let U : ℕ → Submodule ℂ H := fun n ↦ (pi (p n)).range 166 let V : ℕ → Submodule ℂ H := fun n ↦ (pi (q n)).range 167 have hpPi (n : ℕ) : IsStarProjection (pi (p n)) := 168 IsStarProjection.map_representation pi (hp n) 169 have hqPi (n : ℕ) : IsStarProjection (pi (q n)) := 170 IsStarProjection.map_representation pi (hq n) 171 have hUdata (n : ℕ) : ∃ (_ : (U n).HasOrthogonalProjection), 172 pi (p n) = (U n).starProjection := by 173 simpa [U] using 174 (isStarProjection_iff_eq_starProjection_range.mp (hpPi n)) 175 have hVdata (n : ℕ) : ∃ (_ : (V n).HasOrthogonalProjection), 176 pi (q n) = (V n).starProjection := by 177 simpa [V] using 178 (isStarProjection_iff_eq_starProjection_range.mp (hqPi n)) 179 letI hUprojection (n : ℕ) : (U n).HasOrthogonalProjection := 180 (hUdata n).choose 181 letI hVprojection (n : ℕ) : (V n).HasOrthogonalProjection := 182 (hVdata n).choose 183 have hUproj (n : ℕ) : pi (p n) = (U n).starProjection := 184 (hUdata n).choose_spec 185 have hVproj (n : ℕ) : pi (q n) = (V n).starProjection := 186 (hVdata n).choose_spec 187 have hUclosed (n : ℕ) : IsClosed (U n : Set H) := 188 ContinuousLinearMap.IsIdempotentElem.isClosed_range 189 (hpPi n).isIdempotentElem 190 have hVclosed (n : ℕ) : IsClosed (V n : Set H) := 191 ContinuousLinearMap.IsIdempotentElem.isClosed_range 192 (hqPi n).isIdempotentElem 193 letI : IsClosed ((⨅ n, U n : Submodule ℂ H) : Set H) := by 194 simpa only [Submodule.coe_iInf] using isClosed_iInter hUclosed 195 letI : IsClosed ((⨅ n, V n : Submodule ℂ H) : Set H) := by 196 simpa only [Submodule.coe_iInf] using isClosed_iInter hVclosed 197 letI : CompleteSpace (⨅ n, U n : Submodule ℂ H) := inferInstance 198 letI : CompleteSpace (⨅ n, V n : Submodule ℂ H) := inferInstance 199 letI : (⨅ n, U n).HasOrthogonalProjection := inferInstance 200 letI : (⨅ n, V n).HasOrthogonalProjection := inferInstance 201 have hUanti : Antitone U := by 202 intro m n hmn 203 rintro x ⟨y, rfl⟩ 204 refine ⟨pi (p n) y, ?_⟩ 205 have heq : pi (p m) * pi (p n) = pi (p n) := by 206 rw [← map_mul, hp_le hmn] 207 exact congrArg (fun T : H →L[ℂ] H ↦ T y) heq 208 have hVanti : Antitone V := by 209 intro m n hmn 210 rintro x ⟨y, rfl⟩ 211 refine ⟨pi (q n) y, ?_⟩ 212 have heq : pi (q m) * pi (q n) = pi (q n) := by 213 rw [← map_mul, hq_le hmn] 214 exact congrArg (fun T : H →L[ℂ] H ↦ T y) heq 215 have hU0 : U 0 = ⊤ := by 216 rw [← Submodule.range_starProjection (U 0), ← hUproj, hp0, map_one] 217 exact LinearMap.range_eq_top.mpr fun x ↦ ⟨x, rfl⟩ 218 have hV0 : V 0 = ⊤ := by 219 rw [← Submodule.range_starProjection (V 0), ← hVproj, hq0, map_one] 220 exact LinearMap.range_eq_top.mpr fun x ↦ ⟨x, rfl⟩ 221 have hInitialPi (n : ℕ) : 222 ((pi (w n))†).comp (pi (w n)) = Submodule.projectionShell U n := by 223 change star (pi (w n)) * pi (w n) = _ 224 rw [← map_star, ← map_mul, hInitial, map_sub, hUproj, hUproj] 225 rfl 226 have hFinalPi (n : ℕ) : 227 (pi (w n)).comp ((pi (w n))†) = Submodule.projectionShell V n := by 228 change pi (w n) * star (pi (w n)) = _ 229 rw [← map_star, ← map_mul, hFinal, map_sub, hVproj, hVproj] 230 rfl 231 have hShell (n : ℕ) : pi (p n - p (n + 1)) = 232 Submodule.projectionShell U n := by 233 rw [map_sub, hUproj, hUproj] 234 rfl 235 obtain ⟨S, T, hS, hT, hSnorm, hTnorm, hAdj, hProdU, hProdV, 236 hcompletion⟩ := 237 ContinuousLinearMap.exists_strongSums_unitaryCompletion_of_projectionShells 238 e (fun n ↦ pi (w n)) U V hUanti hVanti hU0 hV0 hInitialPi hFinalPi 239 fun n ↦ by 240 rw [← hShell] 241 exact hUnitary n 242 let P : H →L[ℂ] H := (⨅ n, U n).starProjection 243 let Q : H →L[ℂ] H := (⨅ n, V n).starProjection 244 let R : H →L[ℂ] H := (e : H →L[ℂ] H).comp P 245 change (e : H →L[ℂ] H) = S + R ∧ 246 R = (e : H →L[ℂ] H).comp P ∧ 247 (R†).comp R = P ∧ R.comp (R†) = Q ∧ 248 R = (Q.comp R).comp P ∧ 249 (∀ x, x ∈ ⨅ n, U n ↔ e x ∈ ⨅ n, V n) at hcompletion 250 exact ⟨S, T, P, Q, R, hS, hT, hSnorm, hTnorm, hAdj, 251 isStarProjection_starProjection, Submodule.range_starProjection _, 252 isStarProjection_starProjection, Submodule.range_starProjection _, 253 hProdU, hProdV, hcompletion⟩ 254 255end MathlibAnnex.Analysis.CStarAlgebra