Exact source: MathlibAnnex/Analysis/CStarAlgebra/CAR/StateTransport.lean, lines 22–104.
Back to Cross-representation state approximation with a protected finite set · Back to Pure CAR states admit two-sided inner intertwining sequences
1import MathlibAnnex.Analysis.CStarAlgebra.CAR.LocalTransport 2import MathlibAnnex.Analysis.CStarAlgebra.CAR.StagePurification 3 4/-! 5# Local transport of CAR vector states 6 7This file separates the exact same-representation correction from the 8finite-stage approximation used between different representations. The 9protected finite set and its tolerance are fixed before the state tests; a 10later target finite set is handled by finite-stage purification. 11-/ 12 13set_option autoImplicit false 14 15noncomputable section 16 17open MathlibAnnex.Analysis.CStarAlgebra 18 19namespace MathlibAnnex.CStarAlgebra.CAR 20 21set_option maxHeartbeats 800000 in 22/-- A target vector state in another representation can be approximated on 23any later finite set while the implementing inner automorphism nearly fixes 24an earlier protected finite set. Closeness on the fixed stage tests is the 25only hypothesis connecting the two original vector states. -/ 26theorem exists_stageTests_crossRepresentation_path_approx 27 {H : Type*} 28 [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] 29 [Nontrivial H] 30 (rho : Representation Limit H) (hrho : StarAlgHom.IsIrreducible rho) 31 (F : Finset Limit) {epsilon : ℝ} (hepsilon : 0 < epsilon) : 32 ∃ n, ∃ delta > 0, 33 ∀ {K : Type*} 34 [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] 35 (sigma : Representation Limit K) (xi : H) (eta : K), 36 ‖xi‖ = 1 → ‖eta‖ = 1 → 37 (∀ i j : Fin (2 ^ n), 38 ‖Representation.vectorFunctional rho xi (limitMatrixUnit n i j) - 39 Representation.vectorFunctional sigma eta (limitMatrixUnit n i j)‖ < delta) → 40 ∀ (F' : Finset Limit) (epsilon' : ℝ), 0 < epsilon' → 41 ∃ u : unitary Limit, 42 ∃ p : Path 1 u, 43 (∀ t, ∀ a ∈ F, 44 ‖(p t : Limit) * a * star (p t : Limit) - a‖ < epsilon ∧ 45 ‖star (p t : Limit) * a * (p t : Limit) - a‖ < epsilon) ∧ 46 ∀ a ∈ F', 47 ‖Representation.vectorFunctional rho (rho (u : Limit) xi) a - 48 Representation.vectorFunctional sigma eta a‖ < epsilon' := by 49 classical 50 obtain ⟨n, delta, hdelta, hlocal⟩ := 51 exists_stageTests_exact_unitary_path_apply_eq_and_conjugate_sub_norm_lt 52 rho hrho F hepsilon 53 refine ⟨n, delta, hdelta, ?_⟩ 54 intro K _ _ _ sigma xi eta hxi heta hstate F' epsilon' hepsilon' 55 obtain ⟨m, hm⟩ := exists_common_stage_approx F' 56 (show 0 < epsilon' / 3 by positivity) 57 let N : ℕ := max n m 58 have hnN : n ≤ N := le_max_left n m 59 have hmN : m ≤ N := le_max_right n m 60 obtain ⟨zeta, hzeta, hzstage⟩ := 61 exists_unitVector_vectorFunctional_eq_on_stage rho 62 ((Representation.isIrreducible_iff_starAlgHom rho).mpr hrho) 63 sigma N eta heta 64 have hzmatrix (i j : Fin (2 ^ n)) : 65 Representation.vectorFunctional rho zeta (limitMatrixUnit n i j) = 66 Representation.vectorFunctional sigma eta (limitMatrixUnit n i j) := by 67 have h := hzstage (embed n N hnN (matrixUnit n i j)) 68 simpa only [ofStage_embed, limitMatrixUnit] using h 69 obtain ⟨u, huapply, p, huprotect⟩ := hlocal xi zeta hxi hzeta (by 70 intro i j 71 rw [hzmatrix i j] 72 exact hstate i j) 73 refine ⟨u, p, huprotect, ?_⟩ 74 intro a ha 75 obtain ⟨c, hc⟩ := hm a ha 76 let d : Limit := ofStage N (embed m N hmN c) 77 have hd : d = ofStage m c := by 78 dsimp only [d] 79 rw [ofStage_embed] 80 have htarget : 81 Representation.vectorFunctional rho zeta d = 82 Representation.vectorFunctional sigma eta d := by 83 dsimp only [d] 84 exact hzstage (embed m N hmN c) 85 rw [huapply] 86 have hdecomp : 87 Representation.vectorFunctional rho zeta a - 88 Representation.vectorFunctional sigma eta a = 89 Representation.vectorFunctional rho zeta (a - d) + 90 Representation.vectorFunctional sigma eta (d - a) := by 91 rw [map_sub, map_sub, htarget] 92 ring 93 rw [hdecomp] 94 calc 95 _ ≤ ‖Representation.vectorFunctional rho zeta (a - d)‖ + 96 ‖Representation.vectorFunctional sigma eta (d - a)‖ := norm_add_le _ _ 97 _ ≤ ‖a - d‖ + ‖d - a‖ := by 98 exact add_le_add 99 (Representation.norm_vectorFunctional_apply_le rho hzeta (a - d)) 100 (Representation.norm_vectorFunctional_apply_le sigma heta (d - a)) 101 _ = 2 * ‖a - d‖ := by rw [norm_sub_rev d a]; ring 102 _ < epsilon' := by 103 rw [hd] 104 linarith 105 106set_option maxHeartbeats 800000 in 107/-- Endpoint-only compatibility wrapper for 108`exists_stageTests_crossRepresentation_path_approx`. -/ 109theorem exists_stageTests_crossRepresentation_approx 110 {H : Type*} 111 [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] 112 [Nontrivial H] 113 (rho : Representation Limit H) (hrho : StarAlgHom.IsIrreducible rho) 114 (F : Finset Limit) {epsilon : ℝ} (hepsilon : 0 < epsilon) : 115 ∃ n, ∃ delta > 0, 116 ∀ {K : Type*} 117 [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] 118 (sigma : Representation Limit K) (xi : H) (eta : K), 119 ‖xi‖ = 1 → ‖eta‖ = 1 → 120 (∀ i j : Fin (2 ^ n), 121 ‖Representation.vectorFunctional rho xi (limitMatrixUnit n i j) - 122 Representation.vectorFunctional sigma eta (limitMatrixUnit n i j)‖ < delta) → 123 ∀ (F' : Finset Limit) (epsilon' : ℝ), 0 < epsilon' → 124 ∃ u : unitary Limit, 125 (∀ a ∈ F, 126 ‖(u : Limit) * a * star (u : Limit) - a‖ < epsilon ∧ 127 ‖star (u : Limit) * a * (u : Limit) - a‖ < epsilon) ∧ 128 ∀ a ∈ F', 129 ‖Representation.vectorFunctional rho (rho (u : Limit) xi) a - 130 Representation.vectorFunctional sigma eta a‖ < epsilon' := by 131 obtain ⟨n, delta, hdelta, hmain⟩ := 132 exists_stageTests_crossRepresentation_path_approx rho hrho F hepsilon 133 refine ⟨n, delta, hdelta, ?_⟩ 134 intro K _ _ _ sigma xi eta hxi heta hstate F' epsilon' hepsilon' 135 obtain ⟨u, p, hprotect, happrox⟩ := 136 hmain sigma xi eta hxi heta hstate F' epsilon' hepsilon' 137 refine ⟨u, ?_, happrox⟩ 138 intro a ha 139 simpa only [p.target] using hprotect (1 : Set.Icc (0 : ℝ) 1) a ha 140 141set_option maxHeartbeats 800000 in 142/-- With no near-centrality requirement, one irreducible CAR representation 143can approximate an arbitrary unit vector state from another representation on 144any finite set. Stage zero supplies the exact transitivity step, while 145finite-stage purification supplies the requested state accuracy. -/ 146theorem exists_unitary_crossRepresentation_path_approx 147 {H K : Type*} 148 [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] 149 [Nontrivial H] 150 [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] 151 (rho : Representation Limit H) (hrho : StarAlgHom.IsIrreducible rho) 152 (sigma : Representation Limit K) (xi : H) (eta : K) 153 (hxi : ‖xi‖ = 1) (heta : ‖eta‖ = 1) 154 (F : Finset Limit) {epsilon : ℝ} (hepsilon : 0 < epsilon) : 155 ∃ u : unitary Limit, ∃ p : Path 1 u, ∀ a ∈ F, 156 ‖Representation.vectorFunctional rho (rho (u : Limit) xi) a - 157 Representation.vectorFunctional sigma eta a‖ < epsilon := by 158 classical 159 obtain ⟨m, hm⟩ := exists_common_stage_approx F 160 (show 0 < epsilon / 3 by positivity) 161 obtain ⟨zeta, hzeta, hzstage⟩ := 162 exists_unitVector_vectorFunctional_eq_on_stage rho 163 ((Representation.isIrreducible_iff_starAlgHom rho).mpr hrho) 164 sigma m eta heta 165 obtain ⟨delta, hdelta, htrans⟩ := 166 exists_delta_exact_unitary_path_apply_eq_and_stage_commutator 167 rho hrho 0 (by norm_num : (0 : ℝ) < 1) 168 obtain ⟨u, huapply, p, _⟩ := htrans xi zeta hxi hzeta (by 169 intro i j 170 have hunit : limitMatrixUnit 0 (0 : Fin (2 ^ 0)) (0 : Fin (2 ^ 0)) = 1 := by 171 simpa using sum_limitMatrixUnit_diag 0 172 have hij : limitMatrixUnit 0 i j = 1 := by 173 rw [← hunit] 174 congr <;> apply Fin.ext <;> simp 175 rw [hij, Representation.vectorFunctional_one rho hxi, 176 Representation.vectorFunctional_one rho hzeta, sub_self, norm_zero] 177 exact hdelta) 178 refine ⟨u, p, ?_⟩ 179 intro a ha 180 obtain ⟨c, hc⟩ := hm a ha 181 have htarget := hzstage c 182 rw [huapply] 183 have hdecomp : 184 Representation.vectorFunctional rho zeta a - 185 Representation.vectorFunctional sigma eta a = 186 Representation.vectorFunctional rho zeta (a - ofStage m c) + 187 Representation.vectorFunctional sigma eta (ofStage m c - a) := by 188 rw [map_sub, map_sub, htarget] 189 ring 190 rw [hdecomp] 191 calc 192 _ ≤ ‖Representation.vectorFunctional rho zeta (a - ofStage m c)‖ + 193 ‖Representation.vectorFunctional sigma eta (ofStage m c - a)‖ := 194 norm_add_le _ _ 195 _ ≤ ‖a - ofStage m c‖ + ‖ofStage m c - a‖ := by 196 exact add_le_add 197 (Representation.norm_vectorFunctional_apply_le rho hzeta _) 198 (Representation.norm_vectorFunctional_apply_le sigma heta _) 199 _ = 2 * ‖a - ofStage m c‖ := by 200 rw [norm_sub_rev (ofStage m c) a] 201 ring 202 _ < epsilon := by linarith 203 204set_option maxHeartbeats 800000 in 205/-- Endpoint-only compatibility wrapper for 206`exists_unitary_crossRepresentation_path_approx`. -/ 207theorem exists_unitary_crossRepresentation_approx 208 {H K : Type*} 209 [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] 210 [Nontrivial H] 211 [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] 212 (rho : Representation Limit H) (hrho : StarAlgHom.IsIrreducible rho) 213 (sigma : Representation Limit K) (xi : H) (eta : K) 214 (hxi : ‖xi‖ = 1) (heta : ‖eta‖ = 1) 215 (F : Finset Limit) {epsilon : ℝ} (hepsilon : 0 < epsilon) : 216 ∃ u : unitary Limit, ∀ a ∈ F, 217 ‖Representation.vectorFunctional rho (rho (u : Limit) xi) a - 218 Representation.vectorFunctional sigma eta a‖ < epsilon := by 219 obtain ⟨u, -, happrox⟩ := exists_unitary_crossRepresentation_path_approx 220 rho hrho sigma xi eta hxi heta F hepsilon 221 exact ⟨u, happrox⟩ 222 223set_option maxHeartbeats 800000 in 224/-- Pure-state form of cross-representation local transport. For a fixed 225source pure state and protected finite set, the finite stage tests are chosen 226before the target pure state and before the later approximation request. -/ 227theorem exists_stageTests_pureState_path_approx 228 (phi : Limit →L[ℂ] ℂ) (hphi : MathlibAnnex.CStarAlgebra.IsPureState Limit phi) 229 (F : Finset Limit) {epsilon : ℝ} (hepsilon : 0 < epsilon) : 230 ∃ n, ∃ delta > 0, 231 ∀ (psi : Limit →L[ℂ] ℂ), MathlibAnnex.CStarAlgebra.IsPureState Limit psi → 232 (∀ i j : Fin (2 ^ n), 233 ‖phi (limitMatrixUnit n i j) - psi (limitMatrixUnit n i j)‖ < delta) → 234 ∀ (F' : Finset Limit) (epsilon' : ℝ), 0 < epsilon' → 235 ∃ u : unitary Limit, 236 ∃ p : Path 1 u, 237 (∀ t, ∀ a ∈ F, 238 ‖star (p t : Limit) * a * (p t : Limit) - a‖ < epsilon) ∧ 239 ∀ a ∈ F', 240 ‖phi (star (u : Limit) * a * (u : Limit)) - psi a‖ < epsilon' := by 241 have hphiState : phi ∈ stateSpace Limit := extremePoints_subset hphi 242 let fphi := positiveLinearMapOfMemStateSpace phi hphiState 243 let rho : Representation Limit fphi.GNS := fphi.gnsStarAlgHom 244 let xi : fphi.GNS := fphi.gnsCyclicVector 245 have hxi : ‖xi‖ = 1 := by 246 change ‖stateGNSVector phi hphiState‖ = 1 247 exact norm_stateGNSVector phi hphiState 248 letI : Nontrivial fphi.GNS := by 249 apply nontrivial_of_ne xi 0 250 intro hzero 251 have hnorm := congrArg norm hzero 252 rw [hxi, norm_zero] at hnorm 253 norm_num at hnorm 254 have hrho : StarAlgHom.IsIrreducible rho := by 255 simpa [rho, fphi] using 256 isIrreducible_pureState_gnsStarAlgHom phi hphiState hphi 257 have hphiVF : Representation.vectorFunctional rho xi = phi := by 258 apply ContinuousLinearMap.ext 259 intro a 260 rw [Representation.vectorFunctional_apply] 261 change inner ℂ (stateGNSVector phi hphiState) 262 ((positiveLinearMapOfMemStateSpace phi hphiState).gnsStarAlgHom a 263 (stateGNSVector phi hphiState)) = phi a 264 exact inner_gnsStarAlgHom_stateGNSVector phi hphiState a 265 obtain ⟨n, delta, hdelta, hcross⟩ := 266 exists_stageTests_crossRepresentation_path_approx rho hrho F hepsilon 267 refine ⟨n, delta, hdelta, ?_⟩ 268 intro psi hpsi hstate F' epsilon' hepsilon' 269 have hpsiState : psi ∈ stateSpace Limit := extremePoints_subset hpsi 270 let fpsi := positiveLinearMapOfMemStateSpace psi hpsiState 271 let sigma : Representation Limit fpsi.GNS := fpsi.gnsStarAlgHom 272 let eta : fpsi.GNS := fpsi.gnsCyclicVector 273 have heta : ‖eta‖ = 1 := by 274 change ‖stateGNSVector psi hpsiState‖ = 1 275 exact norm_stateGNSVector psi hpsiState 276 have hpsiVF : Representation.vectorFunctional sigma eta = psi := by 277 apply ContinuousLinearMap.ext 278 intro a 279 rw [Representation.vectorFunctional_apply] 280 change inner ℂ (stateGNSVector psi hpsiState) 281 ((positiveLinearMapOfMemStateSpace psi hpsiState).gnsStarAlgHom a 282 (stateGNSVector psi hpsiState)) = psi a 283 exact inner_gnsStarAlgHom_stateGNSVector psi hpsiState a 284 obtain ⟨u, p, hprotect, happrox⟩ := 285 hcross sigma xi eta hxi heta (by 286 intro i j 287 rw [hphiVF, hpsiVF] 288 exact hstate i j) F' epsilon' hepsilon' 289 refine ⟨u, p, (fun t a ha => (hprotect t a ha).2), ?_⟩ 290 intro a ha 291 have h := happrox a ha 292 rw [Representation.vectorFunctional_map_apply, hphiVF, hpsiVF] at h 293 exact h 294 295set_option maxHeartbeats 800000 in 296/-- Endpoint-only compatibility wrapper for 297`exists_stageTests_pureState_path_approx`. -/ 298theorem exists_stageTests_pureState_approx 299 (phi : Limit →L[ℂ] ℂ) (hphi : MathlibAnnex.CStarAlgebra.IsPureState Limit phi) 300 (F : Finset Limit) {epsilon : ℝ} (hepsilon : 0 < epsilon) : 301 ∃ n, ∃ delta > 0, 302 ∀ (psi : Limit →L[ℂ] ℂ), MathlibAnnex.CStarAlgebra.IsPureState Limit psi → 303 (∀ i j : Fin (2 ^ n), 304 ‖phi (limitMatrixUnit n i j) - psi (limitMatrixUnit n i j)‖ < delta) → 305 ∀ (F' : Finset Limit) (epsilon' : ℝ), 0 < epsilon' → 306 ∃ u : unitary Limit, 307 (∀ a ∈ F, 308 ‖star (u : Limit) * a * (u : Limit) - a‖ < epsilon) ∧ 309 ∀ a ∈ F', 310 ‖phi (star (u : Limit) * a * (u : Limit)) - psi a‖ < epsilon' := by 311 obtain ⟨n, delta, hdelta, hmain⟩ := 312 exists_stageTests_pureState_path_approx phi hphi F hepsilon 313 refine ⟨n, delta, hdelta, ?_⟩ 314 intro psi hpsi hstate F' epsilon' hepsilon' 315 obtain ⟨u, p, hprotect, happrox⟩ := 316 hmain psi hpsi hstate F' epsilon' hepsilon' 317 refine ⟨u, ?_, happrox⟩ 318 intro a ha 319 simpa only [p.target] using hprotect (1 : Set.Icc (0 : ℝ) 1) a ha 320 321set_option maxHeartbeats 800000 in 322/-- Any pure CAR state can be approximated on a finite set by an inner 323translate of any other pure state. This is the unprotected initialization 324step for the alternating intertwining construction. -/ 325theorem exists_unitary_pureState_path_approx 326 (phi psi : Limit →L[ℂ] ℂ) 327 (hphi : MathlibAnnex.CStarAlgebra.IsPureState Limit phi) (hpsi : MathlibAnnex.CStarAlgebra.IsPureState Limit psi) 328 (F : Finset Limit) {epsilon : ℝ} (hepsilon : 0 < epsilon) : 329 ∃ u : unitary Limit, ∃ p : Path 1 u, ∀ a ∈ F, 330 ‖phi (star (u : Limit) * a * (u : Limit)) - psi a‖ < epsilon := by 331 have hphiState : phi ∈ stateSpace Limit := extremePoints_subset hphi 332 let fphi := positiveLinearMapOfMemStateSpace phi hphiState 333 let rho : Representation Limit fphi.GNS := fphi.gnsStarAlgHom 334 let xi : fphi.GNS := fphi.gnsCyclicVector 335 have hxi : ‖xi‖ = 1 := by 336 change ‖stateGNSVector phi hphiState‖ = 1 337 exact norm_stateGNSVector phi hphiState 338 letI : Nontrivial fphi.GNS := by 339 apply nontrivial_of_ne xi 0 340 intro hzero 341 have hnorm := congrArg norm hzero 342 rw [hxi, norm_zero] at hnorm 343 norm_num at hnorm 344 have hrho : StarAlgHom.IsIrreducible rho := by 345 simpa [rho, fphi] using 346 isIrreducible_pureState_gnsStarAlgHom phi hphiState hphi 347 have hphiVF : Representation.vectorFunctional rho xi = phi := by 348 apply ContinuousLinearMap.ext 349 intro a 350 rw [Representation.vectorFunctional_apply] 351 change inner ℂ (stateGNSVector phi hphiState) 352 ((positiveLinearMapOfMemStateSpace phi hphiState).gnsStarAlgHom a 353 (stateGNSVector phi hphiState)) = phi a 354 exact inner_gnsStarAlgHom_stateGNSVector phi hphiState a 355 have hpsiState : psi ∈ stateSpace Limit := extremePoints_subset hpsi 356 let fpsi := positiveLinearMapOfMemStateSpace psi hpsiState 357 let sigma : Representation Limit fpsi.GNS := fpsi.gnsStarAlgHom 358 let eta : fpsi.GNS := fpsi.gnsCyclicVector 359 have heta : ‖eta‖ = 1 := by 360 change ‖stateGNSVector psi hpsiState‖ = 1 361 exact norm_stateGNSVector psi hpsiState 362 have hpsiVF : Representation.vectorFunctional sigma eta = psi := by 363 apply ContinuousLinearMap.ext 364 intro a 365 rw [Representation.vectorFunctional_apply] 366 change inner ℂ (stateGNSVector psi hpsiState) 367 ((positiveLinearMapOfMemStateSpace psi hpsiState).gnsStarAlgHom a 368 (stateGNSVector psi hpsiState)) = psi a 369 exact inner_gnsStarAlgHom_stateGNSVector psi hpsiState a 370 obtain ⟨u, p, hu⟩ := exists_unitary_crossRepresentation_path_approx 371 rho hrho sigma xi eta hxi heta F hepsilon 372 refine ⟨u, p, ?_⟩ 373 intro a ha 374 have h := hu a ha 375 rw [Representation.vectorFunctional_map_apply, hphiVF, hpsiVF] at h 376 exact h 377 378set_option maxHeartbeats 800000 in 379/-- Endpoint-only compatibility wrapper for 380`exists_unitary_pureState_path_approx`. -/ 381theorem exists_unitary_pureState_approx 382 (phi psi : Limit →L[ℂ] ℂ) 383 (hphi : MathlibAnnex.CStarAlgebra.IsPureState Limit phi) (hpsi : MathlibAnnex.CStarAlgebra.IsPureState Limit psi) 384 (F : Finset Limit) {epsilon : ℝ} (hepsilon : 0 < epsilon) : 385 ∃ u : unitary Limit, ∀ a ∈ F, 386 ‖phi (star (u : Limit) * a * (u : Limit)) - psi a‖ < epsilon := by 387 obtain ⟨u, -, happrox⟩ := 388 exists_unitary_pureState_path_approx phi psi hphi hpsi F hepsilon 389 exact ⟨u, happrox⟩ 390 391end MathlibAnnex.CStarAlgebra.CAR