Exact source: MathlibAnnex/Analysis/CStarAlgebra/CAR/GlobalTransport.lean, lines 1191–1200.
Back to Pure CAR states admit two-sided inner intertwining sequences
1import MathlibAnnex.Analysis.CStarAlgebra.DenseCauchy 2import MathlibAnnex.Topology.InfinitePath 3import Mathlib.Topology.Algebra.Star.Unitary 4import MathlibAnnex.Analysis.CStarAlgebra.CAR.Homogeneity 5import MathlibAnnex.Analysis.CStarAlgebra.CAR.StateTransport 6 7/-! 8# Alternating global transport for CAR pure states 9 10The local test order is encoded in `AlternatingState`: its movement function 11has already consumed the current stage-test closeness. A transition first 12moves the left vector close on the right tests, then moves the right vector 13close on the next left tests. Thus no future test set is chosen after the 14hypothesis which has to control it. 15-/ 16 17set_option autoImplicit false 18 19noncomputable section 20 21open Filter MathlibAnnex.Analysis.CStarAlgebra TopologicalSpace 22 23namespace MathlibAnnex.CStarAlgebra.CAR 24 25noncomputable def transportDense : ℕ → Limit := denseSeq Limit 26 27theorem denseRange_transportDense : DenseRange transportDense := 28 denseRange_denseSeq Limit 29 30noncomputable def densePrefix (n : ℕ) : Finset Limit := 31 by classical exact (Finset.range (n + 1)).image transportDense 32 33noncomputable def innerAt (u : unitary Limit) : StarAlgEquiv ℂ Limit Limit := 34 Unitary.conjStarAlgAut ℂ Limit (star u) 35 36noncomputable def protectedPrefix (u : unitary Limit) (n : ℕ) : Finset Limit := 37 by classical exact densePrefix n ∪ (densePrefix n).image (innerAt u).symm 38 39noncomputable def stageTests (n : ℕ) : Finset Limit := 40 by 41 classical 42 exact (Finset.univ.product Finset.univ).image 43 (fun ij : Fin (2 ^ n) × Fin (2 ^ n) => limitMatrixUnit n ij.1 ij.2) 44 45def transportBudget (n : ℕ) : ℝ := (1 / 2 : ℝ) ^ n 46 47theorem transportBudget_pos (n : ℕ) : 0 < transportBudget n := by 48 norm_num [transportBudget] 49 50theorem summable_transportBudget : Summable transportBudget := by 51 change Summable fun n : ℕ => (1 / 2 : ℝ) ^ n 52 exact summable_geometric_of_norm_lt_one (by norm_num) 53 54theorem mem_densePrefix {j n : ℕ} (hjn : j ≤ n) : 55 transportDense j ∈ densePrefix n := by 56 classical 57 simp only [densePrefix] 58 apply Finset.mem_image.mpr 59 exact ⟨j, Finset.mem_range.mpr (Nat.lt_succ_of_le hjn), rfl⟩ 60 61theorem mem_protectedPrefix {u : unitary Limit} {j n : ℕ} (hjn : j ≤ n) : 62 transportDense j ∈ protectedPrefix u n := 63 by 64 classical 65 exact Finset.mem_union_left _ (mem_densePrefix hjn) 66 67theorem mem_symm_protectedPrefix {u : unitary Limit} {j n : ℕ} (hjn : j ≤ n) : 68 (innerAt u).symm (transportDense j) ∈ protectedPrefix u n := by 69 classical 70 simp only [protectedPrefix] 71 apply Finset.mem_union_right 72 apply Finset.mem_image.mpr 73 exact ⟨transportDense j, mem_densePrefix hjn, rfl⟩ 74 75theorem mem_stageTests (n : ℕ) (i j : Fin (2 ^ n)) : 76 limitMatrixUnit n i j ∈ stageTests n := by 77 classical 78 simp only [stageTests] 79 apply Finset.mem_image.mpr 80 exact ⟨(i, j), Finset.mem_product.mpr ⟨Finset.mem_univ _, Finset.mem_univ _⟩, rfl⟩ 81 82/-- A recursion state whose left local theorem has already been specialized 83to the current right vector. -/ 84structure AlternatingState 85 {H K : Type*} 86 [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] 87 [Nontrivial H] 88 [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] 89 [Nontrivial K] 90 (rho : Representation Limit H) (sigma : Representation Limit K) 91 (xi : H) (eta : K) (step : ℕ) where 92 left : unitary Limit 93 right : unitary Limit 94 leftPath : Path 1 left 95 rightPath : Path 1 right 96 move : ∀ (F' : Finset Limit) (epsilon' : ℝ), 0 < epsilon' → 97 ∃ u : unitary Limit, 98 ∃ p : Path 1 u, 99 (∀ t, ∀ a ∈ protectedPrefix left step, 100 ‖(p t : Limit) * a * star (p t : Limit) - a‖ < transportBudget step ∧ 101 ‖star (p t : Limit) * a * (p t : Limit) - a‖ < transportBudget step) ∧ 102 ∀ a ∈ F', 103 ‖Representation.vectorFunctional rho 104 (rho (u : Limit) (rho (left : Limit) xi)) a - 105 Representation.vectorFunctional sigma (sigma (right : Limit) eta) a‖ < epsilon' 106 107/-- A transition records both small corrections and the state estimate at 108the left midpoint, before the right correction is applied. -/ 109structure AlternatingTransition 110 {H K : Type*} 111 [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] 112 [Nontrivial H] 113 [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] 114 [Nontrivial K] 115 (rho : Representation Limit H) (sigma : Representation Limit K) 116 (xi : H) (eta : K) {step : ℕ} 117 (s : AlternatingState rho sigma xi eta step) where 118 leftCorrection : unitary Limit 119 rightCorrection : unitary Limit 120 leftCorrectionPath : Path 1 leftCorrection 121 rightCorrectionPath : Path 1 rightCorrection 122 next : AlternatingState rho sigma xi eta (step + 1) 123 next_left : next.left = leftCorrection * s.left 124 next_right : next.right = rightCorrection * s.right 125 left_small : ∀ t, ∀ a ∈ protectedPrefix s.left step, 126 ‖( leftCorrectionPath t : Limit) * a * star (leftCorrectionPath t : Limit) - a‖ < 127 transportBudget step ∧ 128 ‖star (leftCorrectionPath t : Limit) * a * (leftCorrectionPath t : Limit) - a‖ < 129 transportBudget step 130 right_small : ∀ t, ∀ a ∈ protectedPrefix s.right step, 131 ‖( rightCorrectionPath t : Limit) * a * star (rightCorrectionPath t : Limit) - a‖ < 132 transportBudget step ∧ 133 ‖star (rightCorrectionPath t : Limit) * a * (rightCorrectionPath t : Limit) - a‖ < 134 transportBudget step 135 state_small : ∀ j, j ≤ step → 136 ‖Representation.vectorFunctional rho 137 (rho (next.left : Limit) xi) ((innerAt s.right).symm (transportDense j)) - 138 Representation.vectorFunctional sigma 139 (sigma (s.right : Limit) eta) ((innerAt s.right).symm (transportDense j))‖ < 140 transportBudget step 141 142set_option maxHeartbeats 1600000 in 143theorem nonempty_transition 144 {H K : Type*} 145 [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] 146 [Nontrivial H] 147 [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] 148 [Nontrivial K] 149 (rho : Representation Limit H) (hrho : StarAlgHom.IsIrreducible rho) 150 (sigma : Representation Limit K) (hsigma : StarAlgHom.IsIrreducible sigma) 151 (xi : H) (eta : K) (hxi : ‖xi‖ = 1) (heta : ‖eta‖ = 1) 152 {step : ℕ} (s : AlternatingState rho sigma xi eta step) : 153 Nonempty (AlternatingTransition rho sigma xi eta s) := by 154 classical 155 have hleftUnit : ‖rho (s.left : Limit) xi‖ = 1 := by 156 rw [(rho (s.left : Limit)).norm_map_of_mem_unitary 157 (Unitary.map_mem rho s.left.property), hxi] 158 have hrightUnit : ‖sigma (s.right : Limit) eta‖ = 1 := by 159 rw [(sigma (s.right : Limit)).norm_map_of_mem_unitary 160 (Unitary.map_mem sigma s.right.property), heta] 161 obtain ⟨nb, db, hdb, hB⟩ := 162 exists_stageTests_crossRepresentation_path_approx sigma hsigma 163 (protectedPrefix s.right step) (transportBudget_pos step) 164 let requestLeft : Finset Limit := 165 stageTests nb ∪ (densePrefix step).image (innerAt s.right).symm 166 have hmin : 0 < min db (transportBudget step) := lt_min hdb (transportBudget_pos step) 167 obtain ⟨u, pu, husmall, huapprox⟩ := s.move requestLeft _ hmin 168 let left' : unitary Limit := u * s.left 169 let leftSegment : Path s.left left' := 170 { toFun := fun t => pu t * s.left 171 continuous_toFun := by fun_prop 172 source' := by rw [pu.source]; simp 173 target' := by rw [pu.target] } 174 let leftPath' : Path 1 left' := s.leftPath.trans leftSegment 175 have hleft'Unit : ‖rho (left' : Limit) xi‖ = 1 := by 176 rw [(rho (left' : Limit)).norm_map_of_mem_unitary 177 (Unitary.map_mem rho left'.property), hxi] 178 obtain ⟨na, da, hda, hA⟩ := 179 exists_stageTests_crossRepresentation_path_approx rho hrho 180 (protectedPrefix left' (step + 1)) (transportBudget_pos (step + 1)) 181 have hBclose : ∀ i j : Fin (2 ^ nb), 182 ‖Representation.vectorFunctional sigma (sigma (s.right : Limit) eta) 183 (limitMatrixUnit nb i j) - 184 Representation.vectorFunctional rho (rho (left' : Limit) xi) 185 (limitMatrixUnit nb i j)‖ < db := by 186 intro i j 187 have h := huapprox (limitMatrixUnit nb i j) 188 (Finset.mem_union_left _ (mem_stageTests nb i j)) 189 have hsimp : rho (u : Limit) (rho (s.left : Limit) xi) = 190 rho (left' : Limit) xi := by 191 change rho (u : Limit) (rho (s.left : Limit) xi) = 192 rho ((u : Limit) * (s.left : Limit)) xi 193 rw [map_mul, mul_apply_eq_comp] 194 rw [hsimp, norm_sub_rev] at h 195 exact lt_of_lt_of_le h (min_le_left _ _) 196 obtain ⟨v, pv, hvsmall, hvapprox⟩ := 197 hB rho (sigma (s.right : Limit) eta) (rho (left' : Limit) xi) 198 hrightUnit hleft'Unit hBclose (stageTests na) da hda 199 let right' : unitary Limit := v * s.right 200 let rightSegment : Path s.right right' := 201 { toFun := fun t => pv t * s.right 202 continuous_toFun := by fun_prop 203 source' := by rw [pv.source]; simp 204 target' := by rw [pv.target] } 205 let rightPath' : Path 1 right' := s.rightPath.trans rightSegment 206 have hright'Unit : ‖sigma (right' : Limit) eta‖ = 1 := by 207 rw [(sigma (right' : Limit)).norm_map_of_mem_unitary 208 (Unitary.map_mem sigma right'.property), heta] 209 have hAclose : ∀ i j : Fin (2 ^ na), 210 ‖Representation.vectorFunctional rho (rho (left' : Limit) xi) 211 (limitMatrixUnit na i j) - 212 Representation.vectorFunctional sigma (sigma (right' : Limit) eta) 213 (limitMatrixUnit na i j)‖ < da := by 214 intro i j 215 have h := hvapprox (limitMatrixUnit na i j) (mem_stageTests na i j) 216 have hsimp : sigma (v : Limit) (sigma (s.right : Limit) eta) = 217 sigma (right' : Limit) eta := by 218 change sigma (v : Limit) (sigma (s.right : Limit) eta) = 219 sigma ((v : Limit) * (s.right : Limit)) eta 220 rw [map_mul, mul_apply_eq_comp] 221 rw [hsimp, norm_sub_rev] at h 222 exact h 223 let next : AlternatingState rho sigma xi eta (step + 1) := 224 { left := left' 225 right := right' 226 leftPath := leftPath' 227 rightPath := rightPath' 228 move := hA sigma (rho (left' : Limit) xi) (sigma (right' : Limit) eta) 229 hleft'Unit hright'Unit hAclose } 230 refine ⟨{ 231 leftCorrection := u 232 rightCorrection := v 233 leftCorrectionPath := pu 234 rightCorrectionPath := pv 235 next := next 236 next_left := rfl 237 next_right := rfl 238 left_small := husmall 239 right_small := hvsmall 240 state_small := ?_ }⟩ 241 intro j hj 242 have h := huapprox ((innerAt s.right).symm (transportDense j)) 243 (Finset.mem_union_right _ (Finset.mem_image.mpr 244 ⟨transportDense j, mem_densePrefix hj, rfl⟩)) 245 have hsimp : rho (u : Limit) (rho (s.left : Limit) xi) = 246 rho (next.left : Limit) xi := by 247 change rho (u : Limit) (rho (s.left : Limit) xi) = 248 rho ((u : Limit) * (s.left : Limit)) xi 249 rw [map_mul, mul_apply_eq_comp] 250 rw [hsimp] at h 251 exact lt_of_lt_of_le h (min_le_right _ _) 252 253set_option maxHeartbeats 1600000 in 254theorem nonempty_initialState 255 {H K : Type*} 256 [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] 257 [Nontrivial H] 258 [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] 259 [Nontrivial K] 260 (rho : Representation Limit H) (hrho : StarAlgHom.IsIrreducible rho) 261 (sigma : Representation Limit K) (hsigma : StarAlgHom.IsIrreducible sigma) 262 (xi : H) (eta : K) (hxi : ‖xi‖ = 1) (heta : ‖eta‖ = 1) : 263 Nonempty (AlternatingState rho sigma xi eta 0) := by 264 classical 265 obtain ⟨nb, db, hdb, hB⟩ := 266 exists_stageTests_crossRepresentation_path_approx sigma hsigma 267 (protectedPrefix 1 0) (transportBudget_pos 0) 268 obtain ⟨u, pu, hu⟩ := exists_unitary_crossRepresentation_path_approx 269 rho hrho sigma xi eta hxi heta (stageTests nb) hdb 270 let left' : unitary Limit := u 271 have hleft'Unit : ‖rho (left' : Limit) xi‖ = 1 := by 272 rw [(rho (left' : Limit)).norm_map_of_mem_unitary 273 (Unitary.map_mem rho left'.property), hxi] 274 obtain ⟨na, da, hda, hA⟩ := 275 exists_stageTests_crossRepresentation_path_approx rho hrho 276 (protectedPrefix left' 0) (transportBudget_pos 0) 277 have hBclose : ∀ i j : Fin (2 ^ nb), 278 ‖Representation.vectorFunctional sigma eta (limitMatrixUnit nb i j) - 279 Representation.vectorFunctional rho (rho (left' : Limit) xi) 280 (limitMatrixUnit nb i j)‖ < db := by 281 intro i j 282 have h := hu (limitMatrixUnit nb i j) (mem_stageTests nb i j) 283 change ‖Representation.vectorFunctional sigma eta (limitMatrixUnit nb i j) - 284 Representation.vectorFunctional rho (rho (u : Limit) xi) 285 (limitMatrixUnit nb i j)‖ < db 286 rw [norm_sub_rev] 287 exact h 288 obtain ⟨v, pv, _hvsmall, hvapprox⟩ := 289 hB rho eta (rho (left' : Limit) xi) heta hleft'Unit hBclose 290 (stageTests na) da hda 291 let right' : unitary Limit := v 292 have hright'Unit : ‖sigma (right' : Limit) eta‖ = 1 := by 293 rw [(sigma (right' : Limit)).norm_map_of_mem_unitary 294 (Unitary.map_mem sigma right'.property), heta] 295 have hAclose : ∀ i j : Fin (2 ^ na), 296 ‖Representation.vectorFunctional rho (rho (left' : Limit) xi) 297 (limitMatrixUnit na i j) - 298 Representation.vectorFunctional sigma (sigma (right' : Limit) eta) 299 (limitMatrixUnit na i j)‖ < da := by 300 intro i j 301 have h := hvapprox (limitMatrixUnit na i j) (mem_stageTests na i j) 302 change ‖Representation.vectorFunctional rho (rho (left' : Limit) xi) 303 (limitMatrixUnit na i j) - 304 Representation.vectorFunctional sigma (sigma (v : Limit) eta) 305 (limitMatrixUnit na i j)‖ < da 306 rw [norm_sub_rev] 307 exact h 308 exact ⟨{ 309 left := left' 310 right := right' 311 leftPath := pu 312 rightPath := pv 313 move := hA sigma (rho (left' : Limit) xi) (sigma (right' : Limit) eta) 314 hleft'Unit hright'Unit hAclose }⟩ 315 316noncomputable def initialState 317 {H K : Type*} 318 [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] 319 [Nontrivial H] 320 [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] 321 [Nontrivial K] 322 (rho : Representation Limit H) (hrho : StarAlgHom.IsIrreducible rho) 323 (sigma : Representation Limit K) (hsigma : StarAlgHom.IsIrreducible sigma) 324 (xi : H) (eta : K) (hxi : ‖xi‖ = 1) (heta : ‖eta‖ = 1) : 325 AlternatingState rho sigma xi eta 0 := 326 Classical.choice (nonempty_initialState rho hrho sigma hsigma xi eta hxi heta) 327 328noncomputable def chosenTransition 329 {H K : Type*} 330 [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] 331 [Nontrivial H] 332 [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] 333 [Nontrivial K] 334 (rho : Representation Limit H) (hrho : StarAlgHom.IsIrreducible rho) 335 (sigma : Representation Limit K) (hsigma : StarAlgHom.IsIrreducible sigma) 336 (xi : H) (eta : K) (hxi : ‖xi‖ = 1) (heta : ‖eta‖ = 1) 337 {step : ℕ} (s : AlternatingState rho sigma xi eta step) : 338 AlternatingTransition rho sigma xi eta s := 339 Classical.choice (nonempty_transition rho hrho sigma hsigma xi eta hxi heta s) 340 341noncomputable def alternatingStates 342 {H K : Type*} 343 [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] 344 [Nontrivial H] 345 [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] 346 [Nontrivial K] 347 (rho : Representation Limit H) (hrho : StarAlgHom.IsIrreducible rho) 348 (sigma : Representation Limit K) (hsigma : StarAlgHom.IsIrreducible sigma) 349 (xi : H) (eta : K) (hxi : ‖xi‖ = 1) (heta : ‖eta‖ = 1) : 350 (n : ℕ) → AlternatingState rho sigma xi eta n 351 | 0 => initialState rho hrho sigma hsigma xi eta hxi heta 352 | n + 1 => (chosenTransition rho hrho sigma hsigma xi eta hxi heta 353 (alternatingStates rho hrho sigma hsigma xi eta hxi heta n)).next 354 355noncomputable def alternatingTransitions 356 {H K : Type*} 357 [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] 358 [Nontrivial H] 359 [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] 360 [Nontrivial K] 361 (rho : Representation Limit H) (hrho : StarAlgHom.IsIrreducible rho) 362 (sigma : Representation Limit K) (hsigma : StarAlgHom.IsIrreducible sigma) 363 (xi : H) (eta : K) (hxi : ‖xi‖ = 1) (heta : ‖eta‖ = 1) 364 (n : ℕ) : 365 AlternatingTransition rho sigma xi eta 366 (alternatingStates rho hrho sigma hsigma xi eta hxi heta n) := 367 chosenTransition rho hrho sigma hsigma xi eta hxi heta 368 (alternatingStates rho hrho sigma hsigma xi eta hxi heta n) 369 370section Sequences 371 372variable {H K : Type*} 373 [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] 374 [Nontrivial H] 375 [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] 376 [Nontrivial K] 377 (rho : Representation Limit H) (hrho : StarAlgHom.IsIrreducible rho) 378 (sigma : Representation Limit K) (hsigma : StarAlgHom.IsIrreducible sigma) 379 (xi : H) (eta : K) (hxi : ‖xi‖ = 1) (heta : ‖eta‖ = 1) 380 381local notation "S" => alternatingStates rho hrho sigma hsigma xi eta hxi heta 382local notation "T" => alternatingTransitions rho hrho sigma hsigma xi eta hxi heta 383 384/-- Integer-time vertices of the left concatenated path. Negative times are 385constant, time zero is the unit, and time `n+1` is the `n`th recursion state. -/ 386noncomputable def leftPathPoints : ℤ → unitary Limit 387 | .ofNat 0 => 1 388 | .ofNat (n + 1) => (S n).left 389 | .negSucc _ => 1 390 391/-- Integer-time vertices of the right concatenated path. -/ 392noncomputable def rightPathPoints : ℤ → unitary Limit 393 | .ofNat 0 => 1 394 | .ofNat (n + 1) => (S n).right 395 | .negSucc _ => 1 396 397/-- A correction path, translated on the right by the previous accumulated 398unitary. -/ 399def translatedCorrectionPath {u w : unitary Limit} (p : Path 1 u) : 400 Path w (u * w) := 401 { toFun := fun t => p t * w 402 continuous_toFun := by fun_prop 403 source' := by rw [p.source]; simp 404 target' := by rw [p.target] } 405 406/-- Unit-interval pieces of the left unbounded path. -/ 407noncomputable def leftPathSegments : 408 (z : ℤ) → Path 409 (leftPathPoints rho hrho sigma hsigma xi eta hxi heta z) 410 (leftPathPoints rho hrho sigma hsigma xi eta hxi heta (z + 1)) 411 | .ofNat 0 => (S 0).leftPath 412 | .ofNat (n + 1) => by 413 let q : Path (S n).left ((T n).leftCorrection * (S n).left) := 414 translatedCorrectionPath (w := (S n).left) (T n).leftCorrectionPath 415 exact q.cast (by simp [leftPathPoints]) (by 416 simp only [leftPathPoints] 417 change (S (n + 1)).left = (T n).leftCorrection * (S n).left 418 exact (T n).next_left) 419 | .negSucc n => by 420 have hz : Int.negSucc n + 1 = 421 match n with 422 | 0 => (0 : ℤ) 423 | k + 1 => Int.negSucc k := by 424 cases n <;> simp [Int.negSucc_eq] 425 rw [hz] 426 cases n <;> exact Path.refl _ 427 428/-- Unit-interval pieces of the right unbounded path. -/ 429noncomputable def rightPathSegments : 430 (z : ℤ) → Path 431 (rightPathPoints rho hrho sigma hsigma xi eta hxi heta z) 432 (rightPathPoints rho hrho sigma hsigma xi eta hxi heta (z + 1)) 433 | .ofNat 0 => (S 0).rightPath 434 | .ofNat (n + 1) => by 435 let q : Path (S n).right ((T n).rightCorrection * (S n).right) := 436 translatedCorrectionPath (w := (S n).right) (T n).rightCorrectionPath 437 exact q.cast (by simp [rightPathPoints]) (by 438 simp only [rightPathPoints] 439 change (S (n + 1)).right = (T n).rightCorrection * (S n).right 440 exact (T n).next_right) 441 | .negSucc n => by 442 have hz : Int.negSucc n + 1 = 443 match n with 444 | 0 => (0 : ℤ) 445 | k + 1 => Int.negSucc k := by 446 cases n <;> simp [Int.negSucc_eq] 447 rw [hz] 448 cases n <;> exact Path.refl _ 449 450/-- The left locally finite concatenation, constant at negative times. -/ 451noncomputable def leftContinuousPath (t : ℝ) : unitary Limit := 452 MathlibAnnex.Path.infiniteConcat 453 (leftPathPoints rho hrho sigma hsigma xi eta hxi heta) 454 (leftPathSegments rho hrho sigma hsigma xi eta hxi heta) t 455 456/-- The right locally finite concatenation, constant at negative times. -/ 457noncomputable def rightContinuousPath (t : ℝ) : unitary Limit := 458 MathlibAnnex.Path.infiniteConcat 459 (rightPathPoints rho hrho sigma hsigma xi eta hxi heta) 460 (rightPathSegments rho hrho sigma hsigma xi eta hxi heta) t 461 462theorem continuous_leftContinuousPath : 463 Continuous (leftContinuousPath rho hrho sigma hsigma xi eta hxi heta) := 464 MathlibAnnex.Path.continuous_infiniteConcat _ _ 465 466theorem continuous_rightContinuousPath : 467 Continuous (rightContinuousPath rho hrho sigma hsigma xi eta hxi heta) := 468 MathlibAnnex.Path.continuous_infiniteConcat _ _ 469 470theorem leftContinuousPath_zero : 471 leftContinuousPath rho hrho sigma hsigma xi eta hxi heta 0 = 1 := by 472 rw [leftContinuousPath, MathlibAnnex.Path.infiniteConcat, Int.floor_zero] 473 change (S 0).leftPath 474 ⟨Int.fract (0 : ℝ), unitInterval.fract_mem (0 : ℝ)⟩ = 1 475 rw [show (⟨Int.fract (0 : ℝ), unitInterval.fract_mem (0 : ℝ)⟩ : 476 unitInterval) = 0 by ext; norm_num [Int.fract]] 477 exact (S 0).leftPath.source 478 479theorem rightContinuousPath_zero : 480 rightContinuousPath rho hrho sigma hsigma xi eta hxi heta 0 = 1 := by 481 rw [rightContinuousPath, MathlibAnnex.Path.infiniteConcat, Int.floor_zero] 482 change (S 0).rightPath 483 ⟨Int.fract (0 : ℝ), unitInterval.fract_mem (0 : ℝ)⟩ = 1 484 rw [show (⟨Int.fract (0 : ℝ), unitInterval.fract_mem (0 : ℝ)⟩ : 485 unitInterval) = 0 by ext; norm_num [Int.fract]] 486 exact (S 0).rightPath.source 487 488theorem leftContinuousPath_segment (n : ℕ) 489 (t : Set.Icc ((n + 1 : ℕ) : ℝ) (n + 2 : ℝ)) : 490 leftContinuousPath rho hrho sigma hsigma xi eta hxi heta t = 491 (T n).leftCorrectionPath 492 ⟨(t : ℝ) - (n + 1), by 493 constructor 494 · exact sub_nonneg.mpr (by simpa using t.property.1) 495 · apply (sub_le_iff_le_add).mpr 496 have ht := t.property.2 497 linarith⟩ * 498 (S n).left := by 499 let tz : Set.Icc ((Int.ofNat (n + 1) : ℤ) : ℝ) 500 ((Int.ofNat (n + 1) : ℤ) + 1 : ℝ) := 501 ⟨t, by 502 constructor 503 · simpa using t.property.1 504 · have ht := t.property.2 505 norm_num at ht ⊢ 506 linarith⟩ 507 have h := MathlibAnnex.Path.infiniteConcat_eq_intervalPath 508 (leftPathPoints rho hrho sigma hsigma xi eta hxi heta) 509 (leftPathSegments rho hrho sigma hsigma xi eta hxi heta) 510 (Int.ofNat (n + 1)) tz 511 dsimp only [tz] at h 512 convert h using 1 <;> 513 simp [leftContinuousPath, MathlibAnnex.Path.intervalPath, 514 leftPathSegments, translatedCorrectionPath, Path.cast] 515 congr 2 516 517theorem rightContinuousPath_segment (n : ℕ) 518 (t : Set.Icc ((n + 1 : ℕ) : ℝ) (n + 2 : ℝ)) : 519 rightContinuousPath rho hrho sigma hsigma xi eta hxi heta t = 520 (T n).rightCorrectionPath 521 ⟨(t : ℝ) - (n + 1), by 522 constructor 523 · exact sub_nonneg.mpr (by simpa using t.property.1) 524 · apply (sub_le_iff_le_add).mpr 525 have ht := t.property.2 526 linarith⟩ * 527 (S n).right := by 528 let tz : Set.Icc ((Int.ofNat (n + 1) : ℤ) : ℝ) 529 ((Int.ofNat (n + 1) : ℤ) + 1 : ℝ) := 530 ⟨t, by 531 constructor 532 · simpa using t.property.1 533 · have ht := t.property.2 534 norm_num at ht ⊢ 535 linarith⟩ 536 have h := MathlibAnnex.Path.infiniteConcat_eq_intervalPath 537 (rightPathPoints rho hrho sigma hsigma xi eta hxi heta) 538 (rightPathSegments rho hrho sigma hsigma xi eta hxi heta) 539 (Int.ofNat (n + 1)) tz 540 dsimp only [tz] at h 541 convert h using 1 <;> 542 simp [rightContinuousPath, MathlibAnnex.Path.intervalPath, 543 rightPathSegments, translatedCorrectionPath, Path.cast] 544 congr 2 545 546noncomputable def leftAutomorphisms (n : ℕ) : StarAlgEquiv ℂ Limit Limit := 547 innerAt (S n).left 548 549noncomputable def rightAutomorphisms (n : ℕ) : StarAlgEquiv ℂ Limit Limit := 550 innerAt (S n).right 551 552theorem leftContinuousPath_forward_dense_segment (n j : ℕ) (hj : j ≤ n) 553 (t : Set.Icc ((n + 1 : ℕ) : ℝ) (n + 2 : ℝ)) : 554 ‖innerAt (leftContinuousPath rho hrho sigma hsigma xi eta hxi heta t) 555 (transportDense j) - 556 leftAutomorphisms rho hrho sigma hsigma xi eta hxi heta n 557 (transportDense j)‖ ≤ transportBudget n := by 558 let s : unitInterval := 559 ⟨(t : ℝ) - (n + 1), by 560 constructor 561 · exact sub_nonneg.mpr (by simpa using t.property.1) 562 · apply (sub_le_iff_le_add).mpr 563 linarith [t.property.2]⟩ 564 rw [leftContinuousPath_segment rho hrho sigma hsigma xi eta hxi heta n t] 565 have hformula : 566 innerAt ((T n).leftCorrectionPath s * (S n).left) (transportDense j) = 567 innerAt (S n).left 568 (star ((T n).leftCorrectionPath s : Limit) * transportDense j * 569 ((T n).leftCorrectionPath s : Limit)) := by 570 simp [innerAt, mul_assoc] 571 rw [hformula, leftAutomorphisms] 572 calc 573 _ = ‖star ((T n).leftCorrectionPath s : Limit) * transportDense j * 574 ((T n).leftCorrectionPath s : Limit) - transportDense j‖ := by 575 have h := (StarAlgEquiv.isometry (innerAt (S n).left)).dist_eq 576 (star ((T n).leftCorrectionPath s : Limit) * transportDense j * 577 ((T n).leftCorrectionPath s : Limit)) (transportDense j) 578 simpa only [dist_eq_norm] using h 579 _ ≤ transportBudget n := 580 le_of_lt (((T n).left_small s _ (mem_protectedPrefix hj)).2) 581 582theorem leftContinuousPath_inverse_dense_segment (n j : ℕ) (hj : j ≤ n) 583 (t : Set.Icc ((n + 1 : ℕ) : ℝ) (n + 2 : ℝ)) : 584 ‖(innerAt (leftContinuousPath rho hrho sigma hsigma xi eta hxi heta t)).symm 585 (transportDense j) - 586 (leftAutomorphisms rho hrho sigma hsigma xi eta hxi heta n).symm 587 (transportDense j)‖ ≤ transportBudget n := by 588 let s : unitInterval := 589 ⟨(t : ℝ) - (n + 1), by 590 constructor 591 · exact sub_nonneg.mpr (by simpa using t.property.1) 592 · apply (sub_le_iff_le_add).mpr 593 linarith [t.property.2]⟩ 594 rw [leftContinuousPath_segment rho hrho sigma hsigma xi eta hxi heta n t] 595 have hformula : 596 (innerAt ((T n).leftCorrectionPath s * (S n).left)).symm 597 (transportDense j) = 598 ((T n).leftCorrectionPath s : Limit) * 599 (innerAt (S n).left).symm (transportDense j) * 600 star ((T n).leftCorrectionPath s : Limit) := by 601 rw [innerAt, Unitary.conjStarAlgAut_symm, 602 innerAt, Unitary.conjStarAlgAut_symm] 603 simp only [Unitary.conjStarAlgAut_apply, star_star] 604 change (((T n).leftCorrectionPath s : Limit) * (S n).left) * 605 transportDense j * 606 star (((T n).leftCorrectionPath s : Limit) * (S n).left) = _ 607 simp only [star_mul] 608 noncomm_ring 609 rw [hformula, leftAutomorphisms] 610 exact le_of_lt (((T n).left_small s _ (mem_symm_protectedPrefix hj)).1) 611 612theorem rightContinuousPath_forward_dense_segment (n j : ℕ) (hj : j ≤ n) 613 (t : Set.Icc ((n + 1 : ℕ) : ℝ) (n + 2 : ℝ)) : 614 ‖innerAt (rightContinuousPath rho hrho sigma hsigma xi eta hxi heta t) 615 (transportDense j) - 616 rightAutomorphisms rho hrho sigma hsigma xi eta hxi heta n 617 (transportDense j)‖ ≤ transportBudget n := by 618 let s : unitInterval := 619 ⟨(t : ℝ) - (n + 1), by 620 constructor 621 · exact sub_nonneg.mpr (by simpa using t.property.1) 622 · apply (sub_le_iff_le_add).mpr 623 linarith [t.property.2]⟩ 624 rw [rightContinuousPath_segment rho hrho sigma hsigma xi eta hxi heta n t] 625 have hformula : 626 innerAt ((T n).rightCorrectionPath s * (S n).right) (transportDense j) = 627 innerAt (S n).right 628 (star ((T n).rightCorrectionPath s : Limit) * transportDense j * 629 ((T n).rightCorrectionPath s : Limit)) := by 630 simp [innerAt, mul_assoc] 631 rw [hformula, rightAutomorphisms] 632 calc 633 _ = ‖star ((T n).rightCorrectionPath s : Limit) * transportDense j * 634 ((T n).rightCorrectionPath s : Limit) - transportDense j‖ := by 635 have h := (StarAlgEquiv.isometry (innerAt (S n).right)).dist_eq 636 (star ((T n).rightCorrectionPath s : Limit) * transportDense j * 637 ((T n).rightCorrectionPath s : Limit)) (transportDense j) 638 simpa only [dist_eq_norm] using h 639 _ ≤ transportBudget n := 640 le_of_lt (((T n).right_small s _ (mem_protectedPrefix hj)).2) 641 642theorem rightContinuousPath_inverse_dense_segment (n j : ℕ) (hj : j ≤ n) 643 (t : Set.Icc ((n + 1 : ℕ) : ℝ) (n + 2 : ℝ)) : 644 ‖(innerAt (rightContinuousPath rho hrho sigma hsigma xi eta hxi heta t)).symm 645 (transportDense j) - 646 (rightAutomorphisms rho hrho sigma hsigma xi eta hxi heta n).symm 647 (transportDense j)‖ ≤ transportBudget n := by 648 let s : unitInterval := 649 ⟨(t : ℝ) - (n + 1), by 650 constructor 651 · exact sub_nonneg.mpr (by simpa using t.property.1) 652 · apply (sub_le_iff_le_add).mpr 653 linarith [t.property.2]⟩ 654 rw [rightContinuousPath_segment rho hrho sigma hsigma xi eta hxi heta n t] 655 have hformula : 656 (innerAt ((T n).rightCorrectionPath s * (S n).right)).symm 657 (transportDense j) = 658 ((T n).rightCorrectionPath s : Limit) * 659 (innerAt (S n).right).symm (transportDense j) * 660 star ((T n).rightCorrectionPath s : Limit) := by 661 rw [innerAt, Unitary.conjStarAlgAut_symm, 662 innerAt, Unitary.conjStarAlgAut_symm] 663 simp only [Unitary.conjStarAlgAut_apply, star_star] 664 change (((T n).rightCorrectionPath s : Limit) * (S n).right) * 665 transportDense j * 666 star (((T n).rightCorrectionPath s : Limit) * (S n).right) = _ 667 simp only [star_mul] 668 noncomm_ring 669 rw [hformula, rightAutomorphisms] 670 exact le_of_lt (((T n).right_small s _ (mem_symm_protectedPrefix hj)).1) 671 672theorem leftAutomorphisms_step (n j : ℕ) (hj : j ≤ n) : 673 ‖leftAutomorphisms rho hrho sigma hsigma xi eta hxi heta (n + 1) 674 (transportDense j) - 675 leftAutomorphisms rho hrho sigma hsigma xi eta hxi heta n 676 (transportDense j)‖ ≤ transportBudget n := by 677 let t := T n 678 have hnext : S (n + 1) = t.next := rfl 679 rw [leftAutomorphisms, leftAutomorphisms, hnext, t.next_left] 680 have hformula : 681 innerAt (t.leftCorrection * (S n).left) (transportDense j) = 682 innerAt (S n).left 683 (star (t.leftCorrection : Limit) * transportDense j * 684 (t.leftCorrection : Limit)) := by 685 simp [innerAt, mul_assoc] 686 rw [hformula] 687 calc 688 _ = ‖star (t.leftCorrection : Limit) * transportDense j * 689 (t.leftCorrection : Limit) - transportDense j‖ := by 690 have h := (StarAlgEquiv.isometry (innerAt (S n).left)).dist_eq 691 (star (t.leftCorrection : Limit) * transportDense j * 692 (t.leftCorrection : Limit)) (transportDense j) 693 simpa only [dist_eq_norm] using h 694 _ ≤ transportBudget n := by 695 have h := (t.left_small (1 : Set.Icc (0 : ℝ) 1) _ 696 (mem_protectedPrefix hj)).2 697 simpa only [t.leftCorrectionPath.target] using le_of_lt h 698 699theorem leftAutomorphisms_symm_step (n j : ℕ) (hj : j ≤ n) : 700 ‖(leftAutomorphisms rho hrho sigma hsigma xi eta hxi heta (n + 1)).symm 701 (transportDense j) - 702 (leftAutomorphisms rho hrho sigma hsigma xi eta hxi heta n).symm 703 (transportDense j)‖ ≤ transportBudget n := by 704 let t := T n 705 have hnext : S (n + 1) = t.next := rfl 706 rw [leftAutomorphisms, leftAutomorphisms, hnext, t.next_left] 707 have hformula : 708 (innerAt (t.leftCorrection * (S n).left)).symm (transportDense j) = 709 (t.leftCorrection : Limit) * 710 (innerAt (S n).left).symm (transportDense j) * 711 star (t.leftCorrection : Limit) := by 712 rw [innerAt, Unitary.conjStarAlgAut_symm, 713 innerAt, Unitary.conjStarAlgAut_symm] 714 simp only [Unitary.conjStarAlgAut_apply, star_star] 715 change ((t.leftCorrection : Limit) * (S n).left) * transportDense j * 716 star ((t.leftCorrection : Limit) * (S n).left) = _ 717 simp only [star_mul] 718 noncomm_ring 719 rw [hformula] 720 have h := (t.left_small (1 : Set.Icc (0 : ℝ) 1) _ 721 (mem_symm_protectedPrefix hj)).1 722 simpa only [t.leftCorrectionPath.target] using le_of_lt h 723 724theorem rightAutomorphisms_step (n j : ℕ) (hj : j ≤ n) : 725 ‖rightAutomorphisms rho hrho sigma hsigma xi eta hxi heta (n + 1) 726 (transportDense j) - 727 rightAutomorphisms rho hrho sigma hsigma xi eta hxi heta n 728 (transportDense j)‖ ≤ transportBudget n := by 729 let t := T n 730 have hnext : S (n + 1) = t.next := rfl 731 rw [rightAutomorphisms, rightAutomorphisms, hnext, t.next_right] 732 have hformula : 733 innerAt (t.rightCorrection * (S n).right) (transportDense j) = 734 innerAt (S n).right 735 (star (t.rightCorrection : Limit) * transportDense j * 736 (t.rightCorrection : Limit)) := by 737 simp [innerAt, mul_assoc] 738 rw [hformula] 739 calc 740 _ = ‖star (t.rightCorrection : Limit) * transportDense j * 741 (t.rightCorrection : Limit) - transportDense j‖ := by 742 have h := (StarAlgEquiv.isometry (innerAt (S n).right)).dist_eq 743 (star (t.rightCorrection : Limit) * transportDense j * 744 (t.rightCorrection : Limit)) (transportDense j) 745 simpa only [dist_eq_norm] using h 746 _ ≤ transportBudget n := by 747 have h := (t.right_small (1 : Set.Icc (0 : ℝ) 1) _ 748 (mem_protectedPrefix hj)).2 749 simpa only [t.rightCorrectionPath.target] using le_of_lt h 750 751theorem rightAutomorphisms_symm_step (n j : ℕ) (hj : j ≤ n) : 752 ‖(rightAutomorphisms rho hrho sigma hsigma xi eta hxi heta (n + 1)).symm 753 (transportDense j) - 754 (rightAutomorphisms rho hrho sigma hsigma xi eta hxi heta n).symm 755 (transportDense j)‖ ≤ transportBudget n := by 756 let t := T n 757 have hnext : S (n + 1) = t.next := rfl 758 rw [rightAutomorphisms, rightAutomorphisms, hnext, t.next_right] 759 have hformula : 760 (innerAt (t.rightCorrection * (S n).right)).symm (transportDense j) = 761 (t.rightCorrection : Limit) * 762 (innerAt (S n).right).symm (transportDense j) * 763 star (t.rightCorrection : Limit) := by 764 rw [innerAt, Unitary.conjStarAlgAut_symm, 765 innerAt, Unitary.conjStarAlgAut_symm] 766 simp only [Unitary.conjStarAlgAut_apply, star_star] 767 change ((t.rightCorrection : Limit) * (S n).right) * transportDense j * 768 star ((t.rightCorrection : Limit) * (S n).right) = _ 769 simp only [star_mul] 770 noncomm_ring 771 rw [hformula] 772 have h := (t.right_small (1 : Set.Icc (0 : ℝ) 1) _ 773 (mem_symm_protectedPrefix hj)).1 774 simpa only [t.rightCorrectionPath.target] using le_of_lt h 775 776theorem leftAutomorphisms_cauchy : 777 ∀ a, CauchySeq (fun n => 778 leftAutomorphisms rho hrho sigma hsigma xi eta hxi heta n a) := 779 MathlibAnnex.CStarAlgebra.cauchySeq_of_summable_dense_steps 780 transportDense denseRange_transportDense 781 (leftAutomorphisms rho hrho sigma hsigma xi eta hxi heta) 782 transportBudget summable_transportBudget 783 (leftAutomorphisms_step rho hrho sigma hsigma xi eta hxi heta) 784 785theorem leftAutomorphisms_symm_cauchy : 786 ∀ a, CauchySeq (fun n => 787 (leftAutomorphisms rho hrho sigma hsigma xi eta hxi heta n).symm a) := 788 MathlibAnnex.CStarAlgebra.cauchySeq_of_summable_dense_steps 789 transportDense denseRange_transportDense 790 (fun n => (leftAutomorphisms rho hrho sigma hsigma xi eta hxi heta n).symm) 791 transportBudget summable_transportBudget 792 (leftAutomorphisms_symm_step rho hrho sigma hsigma xi eta hxi heta) 793 794theorem rightAutomorphisms_cauchy : 795 ∀ a, CauchySeq (fun n => 796 rightAutomorphisms rho hrho sigma hsigma xi eta hxi heta n a) := 797 MathlibAnnex.CStarAlgebra.cauchySeq_of_summable_dense_steps 798 transportDense denseRange_transportDense 799 (rightAutomorphisms rho hrho sigma hsigma xi eta hxi heta) 800 transportBudget summable_transportBudget 801 (rightAutomorphisms_step rho hrho sigma hsigma xi eta hxi heta) 802 803theorem rightAutomorphisms_symm_cauchy : 804 ∀ a, CauchySeq (fun n => 805 (rightAutomorphisms rho hrho sigma hsigma xi eta hxi heta n).symm a) := 806 MathlibAnnex.CStarAlgebra.cauchySeq_of_summable_dense_steps 807 transportDense denseRange_transportDense 808 (fun n => (rightAutomorphisms rho hrho sigma hsigma xi eta hxi heta n).symm) 809 transportBudget summable_transportBudget 810 (rightAutomorphisms_symm_step rho hrho sigma hsigma xi eta hxi heta) 811 812theorem tendsto_transportBudget_zero : 813 Tendsto transportBudget atTop (nhds 0) := by 814 change Tendsto (fun n : ℕ => (1 / 2 : ℝ) ^ n) atTop (nhds 0) 815 exact tendsto_pow_atTop_nhds_zero_of_lt_one (by norm_num) (by norm_num) 816 817/-- The two-sided pointwise limit of the accumulated left conjugations. -/ 818noncomputable def leftLimitAutomorphism : StarAlgEquiv ℂ Limit Limit := 819 MathlibAnnex.CStarAlgebra.twoSidedPointwiseLimit 820 (leftAutomorphisms rho hrho sigma hsigma xi eta hxi heta) 821 (leftAutomorphisms_cauchy rho hrho sigma hsigma xi eta hxi heta) 822 (leftAutomorphisms_symm_cauchy rho hrho sigma hsigma xi eta hxi heta) 823 824/-- The two-sided pointwise limit of the accumulated right conjugations. -/ 825noncomputable def rightLimitAutomorphism : StarAlgEquiv ℂ Limit Limit := 826 MathlibAnnex.CStarAlgebra.twoSidedPointwiseLimit 827 (rightAutomorphisms rho hrho sigma hsigma xi eta hxi heta) 828 (rightAutomorphisms_cauchy rho hrho sigma hsigma xi eta hxi heta) 829 (rightAutomorphisms_symm_cauchy rho hrho sigma hsigma xi eta hxi heta) 830 831theorem tendsto_leftContinuousPath_forward (a : Limit) : 832 Tendsto (fun t : ℝ => 833 innerAt (leftContinuousPath rho hrho sigma hsigma xi eta hxi heta t) a) 834 atTop (nhds (leftLimitAutomorphism rho hrho sigma hsigma xi eta hxi heta a)) := by 835 apply MathlibAnnex.Metric.tendsto_atTop_of_isometry_segment_approx 836 transportDense denseRange_transportDense 837 (fun n a => leftAutomorphisms rho hrho sigma hsigma xi eta hxi heta n a) 838 (fun t => innerAt (leftContinuousPath rho hrho sigma hsigma xi eta hxi heta t)) 839 (fun n => StarAlgEquiv.isometry 840 (leftAutomorphisms rho hrho sigma hsigma xi eta hxi heta n)) 841 (fun t => StarAlgEquiv.isometry 842 (innerAt (leftContinuousPath rho hrho sigma hsigma xi eta hxi heta t))) 843 transportBudget tendsto_transportBudget_zero 844 (fun n j hj t => by 845 simpa only [dist_eq_norm] using 846 leftContinuousPath_forward_dense_segment 847 rho hrho sigma hsigma xi eta hxi heta n j hj t) 848 a _ 849 simpa [leftLimitAutomorphism, 850 MathlibAnnex.CStarAlgebra.twoSidedPointwiseLimit_apply, 851 MathlibAnnex.CStarAlgebra.pointwiseLimitHom_apply] using 852 MathlibAnnex.CStarAlgebra.tendsto_pointwiseLimit 853 (leftAutomorphisms rho hrho sigma hsigma xi eta hxi heta) 854 (leftAutomorphisms_cauchy rho hrho sigma hsigma xi eta hxi heta) a 855 856theorem tendsto_leftContinuousPath_inverse (a : Limit) : 857 Tendsto (fun t : ℝ => 858 (innerAt (leftContinuousPath rho hrho sigma hsigma xi eta hxi heta t)).symm a) 859 atTop (nhds ((leftLimitAutomorphism 860 rho hrho sigma hsigma xi eta hxi heta).symm a)) := by 861 apply MathlibAnnex.Metric.tendsto_atTop_of_isometry_segment_approx 862 transportDense denseRange_transportDense 863 (fun n a => 864 (leftAutomorphisms rho hrho sigma hsigma xi eta hxi heta n).symm a) 865 (fun t => (innerAt 866 (leftContinuousPath rho hrho sigma hsigma xi eta hxi heta t)).symm) 867 (fun n => StarAlgEquiv.isometry 868 (leftAutomorphisms rho hrho sigma hsigma xi eta hxi heta n).symm) 869 (fun t => StarAlgEquiv.isometry 870 (innerAt (leftContinuousPath rho hrho sigma hsigma xi eta hxi heta t)).symm) 871 transportBudget tendsto_transportBudget_zero 872 (fun n j hj t => by 873 simpa only [dist_eq_norm] using 874 leftContinuousPath_inverse_dense_segment 875 rho hrho sigma hsigma xi eta hxi heta n j hj t) 876 a _ 877 rw [leftLimitAutomorphism, 878 MathlibAnnex.CStarAlgebra.twoSidedPointwiseLimit_symm_apply] 879 exact MathlibAnnex.CStarAlgebra.tendsto_pointwiseLimit 880 (fun n => (leftAutomorphisms rho hrho sigma hsigma xi eta hxi heta n).symm) 881 (leftAutomorphisms_symm_cauchy rho hrho sigma hsigma xi eta hxi heta) a 882 883theorem tendsto_rightContinuousPath_forward (a : Limit) : 884 Tendsto (fun t : ℝ => 885 innerAt (rightContinuousPath rho hrho sigma hsigma xi eta hxi heta t) a) 886 atTop (nhds (rightLimitAutomorphism rho hrho sigma hsigma xi eta hxi heta a)) := by 887 apply MathlibAnnex.Metric.tendsto_atTop_of_isometry_segment_approx 888 transportDense denseRange_transportDense 889 (fun n a => rightAutomorphisms rho hrho sigma hsigma xi eta hxi heta n a) 890 (fun t => innerAt (rightContinuousPath rho hrho sigma hsigma xi eta hxi heta t)) 891 (fun n => StarAlgEquiv.isometry 892 (rightAutomorphisms rho hrho sigma hsigma xi eta hxi heta n)) 893 (fun t => StarAlgEquiv.isometry 894 (innerAt (rightContinuousPath rho hrho sigma hsigma xi eta hxi heta t))) 895 transportBudget tendsto_transportBudget_zero 896 (fun n j hj t => by 897 simpa only [dist_eq_norm] using 898 rightContinuousPath_forward_dense_segment 899 rho hrho sigma hsigma xi eta hxi heta n j hj t) 900 a _ 901 simpa [rightLimitAutomorphism, 902 MathlibAnnex.CStarAlgebra.twoSidedPointwiseLimit_apply, 903 MathlibAnnex.CStarAlgebra.pointwiseLimitHom_apply] using 904 MathlibAnnex.CStarAlgebra.tendsto_pointwiseLimit 905 (rightAutomorphisms rho hrho sigma hsigma xi eta hxi heta) 906 (rightAutomorphisms_cauchy rho hrho sigma hsigma xi eta hxi heta) a 907 908theorem tendsto_rightContinuousPath_inverse (a : Limit) : 909 Tendsto (fun t : ℝ => 910 (innerAt (rightContinuousPath rho hrho sigma hsigma xi eta hxi heta t)).symm a) 911 atTop (nhds ((rightLimitAutomorphism 912 rho hrho sigma hsigma xi eta hxi heta).symm a)) := by 913 apply MathlibAnnex.Metric.tendsto_atTop_of_isometry_segment_approx 914 transportDense denseRange_transportDense 915 (fun n a => 916 (rightAutomorphisms rho hrho sigma hsigma xi eta hxi heta n).symm a) 917 (fun t => (innerAt 918 (rightContinuousPath rho hrho sigma hsigma xi eta hxi heta t)).symm) 919 (fun n => StarAlgEquiv.isometry 920 (rightAutomorphisms rho hrho sigma hsigma xi eta hxi heta n).symm) 921 (fun t => StarAlgEquiv.isometry 922 (innerAt (rightContinuousPath rho hrho sigma hsigma xi eta hxi heta t)).symm) 923 transportBudget tendsto_transportBudget_zero 924 (fun n j hj t => by 925 simpa only [dist_eq_norm] using 926 rightContinuousPath_inverse_dense_segment 927 rho hrho sigma hsigma xi eta hxi heta n j hj t) 928 a _ 929 rw [rightLimitAutomorphism, 930 MathlibAnnex.CStarAlgebra.twoSidedPointwiseLimit_symm_apply] 931 exact MathlibAnnex.CStarAlgebra.tendsto_pointwiseLimit 932 (fun n => (rightAutomorphisms rho hrho sigma hsigma xi eta hxi heta n).symm) 933 (rightAutomorphisms_symm_cauchy rho hrho sigma hsigma xi eta hxi heta) a 934 935noncomputable def outputUnitary (n : ℕ) : unitary Limit := 936 star (S (n + 1)).left * (S n).right 937 938noncomputable def outputAutomorphisms (n : ℕ) : StarAlgEquiv ℂ Limit Limit := 939 Unitary.conjStarAlgAut ℂ Limit 940 (outputUnitary rho hrho sigma hsigma xi eta hxi heta n) 941 942theorem outputAutomorphisms_eq (n : ℕ) : 943 outputAutomorphisms rho hrho sigma hsigma xi eta hxi heta n = 944 (rightAutomorphisms rho hrho sigma hsigma xi eta hxi heta n).symm.trans 945 (leftAutomorphisms rho hrho sigma hsigma xi eta hxi heta (n + 1)) := by 946 ext a 947 simp [outputAutomorphisms, outputUnitary, rightAutomorphisms, 948 leftAutomorphisms, innerAt, mul_assoc] 949 950theorem leftAutomorphisms_succ_cauchy : 951 ∀ a, CauchySeq (fun n => 952 leftAutomorphisms rho hrho sigma hsigma xi eta hxi heta (n + 1) a) := by 953 intro a 954 exact (cauchySeq_shift 1).2 955 (leftAutomorphisms_cauchy rho hrho sigma hsigma xi eta hxi heta a) 956 957theorem leftAutomorphisms_succ_symm_cauchy : 958 ∀ a, CauchySeq (fun n => 959 (leftAutomorphisms rho hrho sigma hsigma xi eta hxi heta (n + 1)).symm a) := by 960 intro a 961 exact (cauchySeq_shift 1).2 962 (leftAutomorphisms_symm_cauchy rho hrho sigma hsigma xi eta hxi heta a) 963 964theorem outputAutomorphisms_cauchy : 965 ∀ a, CauchySeq (fun n => 966 outputAutomorphisms rho hrho sigma hsigma xi eta hxi heta n a) := by 967 intro a 968 have h := MathlibAnnex.CStarAlgebra.cauchySeq_trans_of_isometry 969 (fun n => leftAutomorphisms rho hrho sigma hsigma xi eta hxi heta (n + 1)) 970 (fun n => (rightAutomorphisms rho hrho sigma hsigma xi eta hxi heta n).symm) 971 (leftAutomorphisms_succ_cauchy rho hrho sigma hsigma xi eta hxi heta) 972 (rightAutomorphisms_symm_cauchy rho hrho sigma hsigma xi eta hxi heta) a 973 simpa only [outputAutomorphisms_eq] using h 974 975theorem outputAutomorphisms_symm_cauchy : 976 ∀ a, CauchySeq (fun n => 977 (outputAutomorphisms rho hrho sigma hsigma xi eta hxi heta n).symm a) := by 978 intro a 979 have h := MathlibAnnex.CStarAlgebra.cauchySeq_trans_of_isometry 980 (rightAutomorphisms rho hrho sigma hsigma xi eta hxi heta) 981 (fun n => 982 (leftAutomorphisms rho hrho sigma hsigma xi eta hxi heta (n + 1)).symm) 983 (rightAutomorphisms_cauchy rho hrho sigma hsigma xi eta hxi heta) 984 (leftAutomorphisms_succ_symm_cauchy rho hrho sigma hsigma xi eta hxi heta) a 985 have heq : ∀ n, 986 (outputAutomorphisms rho hrho sigma hsigma xi eta hxi heta n).symm = 987 (leftAutomorphisms rho hrho sigma hsigma xi eta hxi heta (n + 1)).symm.trans 988 (rightAutomorphisms rho hrho sigma hsigma xi eta hxi heta n) := by 989 intro n 990 rw [outputAutomorphisms_eq] 991 rfl 992 simpa only [heq] using h 993 994theorem outputAutomorphisms_state_dense (n j : ℕ) (hj : j ≤ n) : 995 ‖Representation.vectorFunctional rho xi 996 (outputAutomorphisms rho hrho sigma hsigma xi eta hxi heta n 997 (transportDense j)) - 998 Representation.vectorFunctional sigma eta (transportDense j)‖ < 999 transportBudget n := by 1000 let t := T n 1001 have hnext : S (n + 1) = t.next := rfl 1002 have h := t.state_small j hj 1003 rw [← hnext] at h 1004 rw [Representation.vectorFunctional_map_apply, 1005 Representation.vectorFunctional_map_apply] at h 1006 have h' : 1007 ‖Representation.vectorFunctional rho xi 1008 (innerAt (S (n + 1)).left 1009 ((innerAt (S n).right).symm (transportDense j))) - 1010 Representation.vectorFunctional sigma eta 1011 (innerAt (S n).right 1012 ((innerAt (S n).right).symm (transportDense j)))‖ < 1013 transportBudget n := by 1014 simpa [innerAt] using h 1015 have hleft : 1016 innerAt (S (n + 1)).left 1017 ((innerAt (S n).right).symm (transportDense j)) = 1018 outputAutomorphisms rho hrho sigma hsigma xi eta hxi heta n 1019 (transportDense j) := by 1020 rw [outputAutomorphisms_eq] 1021 rfl 1022 rw [hleft, (innerAt (S n).right).apply_symm_apply] at h' 1023 exact h' 1024 1025theorem tendsto_outputAutomorphisms_state : 1026 ∀ a, Tendsto (fun n => Representation.vectorFunctional rho xi 1027 (outputAutomorphisms rho hrho sigma hsigma xi eta hxi heta n a)) 1028 atTop (nhds (Representation.vectorFunctional sigma eta a)) := by 1029 apply MathlibAnnex.CStarAlgebra.tendsto_functional_of_dense_prefix 1030 transportDense denseRange_transportDense 1031 (outputAutomorphisms rho hrho sigma hsigma xi eta hxi heta) 1032 (Representation.vectorFunctional rho xi) 1033 (Representation.vectorFunctional sigma eta) 1034 (Representation.norm_vectorFunctional_apply_le rho hxi) 1035 (Representation.norm_vectorFunctional_apply_le sigma heta) 1036 transportBudget tendsto_transportBudget_zero 1037 exact outputAutomorphisms_state_dense rho hrho sigma hsigma xi eta hxi heta 1038 1039/-- The common limit written using equal-time left and right limits. -/ 1040noncomputable def asymptoticAutomorphism : StarAlgEquiv ℂ Limit Limit := 1041 (rightLimitAutomorphism rho hrho sigma hsigma xi eta hxi heta).symm.trans 1042 (leftLimitAutomorphism rho hrho sigma hsigma xi eta hxi heta) 1043 1044/-- The norm-continuous implementing unitary path. -/ 1045noncomputable def implementingUnitary (t : ℝ) : unitary Limit := 1046 star (leftContinuousPath rho hrho sigma hsigma xi eta hxi heta t) * 1047 rightContinuousPath rho hrho sigma hsigma xi eta hxi heta t 1048 1049noncomputable def implementingAutomorphism (t : ℝ) : StarAlgEquiv ℂ Limit Limit := 1050 Unitary.conjStarAlgAut ℂ Limit 1051 (implementingUnitary rho hrho sigma hsigma xi eta hxi heta t) 1052 1053theorem continuous_implementingUnitary : 1054 Continuous (implementingUnitary rho hrho sigma hsigma xi eta hxi heta) := by 1055 unfold implementingUnitary 1056 change Continuous (fun t => 1057 (leftContinuousPath rho hrho sigma hsigma xi eta hxi heta t)⁻¹ * 1058 rightContinuousPath rho hrho sigma hsigma xi eta hxi heta t) 1059 exact (continuous_leftContinuousPath 1060 rho hrho sigma hsigma xi eta hxi heta).inv.mul 1061 (continuous_rightContinuousPath rho hrho sigma hsigma xi eta hxi heta) 1062 1063theorem implementingUnitary_zero : 1064 implementingUnitary rho hrho sigma hsigma xi eta hxi heta 0 = 1 := by 1065 simp [implementingUnitary, 1066 leftContinuousPath_zero rho hrho sigma hsigma xi eta hxi heta, 1067 rightContinuousPath_zero rho hrho sigma hsigma xi eta hxi heta] 1068 1069theorem implementingAutomorphism_eq (t : ℝ) : 1070 implementingAutomorphism rho hrho sigma hsigma xi eta hxi heta t = 1071 (innerAt (rightContinuousPath rho hrho sigma hsigma xi eta hxi heta t)).symm.trans 1072 (innerAt (leftContinuousPath rho hrho sigma hsigma xi eta hxi heta t)) := by 1073 ext a 1074 simp [implementingAutomorphism, implementingUnitary, innerAt, mul_assoc] 1075 1076theorem implementingAutomorphism_symm_eq (t : ℝ) : 1077 (implementingAutomorphism rho hrho sigma hsigma xi eta hxi heta t).symm = 1078 (innerAt (leftContinuousPath rho hrho sigma hsigma xi eta hxi heta t)).symm.trans 1079 (innerAt (rightContinuousPath rho hrho sigma hsigma xi eta hxi heta t)) := by 1080 rw [implementingAutomorphism_eq] 1081 rfl 1082 1083theorem tendsto_outputAutomorphisms_asymptoticAutomorphism (a : Limit) : 1084 Tendsto (fun n => outputAutomorphisms 1085 rho hrho sigma hsigma xi eta hxi heta n a) 1086 atTop (nhds (asymptoticAutomorphism 1087 rho hrho sigma hsigma xi eta hxi heta a)) := by 1088 have hright : Tendsto (fun n => 1089 (rightAutomorphisms rho hrho sigma hsigma xi eta hxi heta n).symm a) 1090 atTop (nhds ((rightLimitAutomorphism 1091 rho hrho sigma hsigma xi eta hxi heta).symm a)) := by 1092 rw [rightLimitAutomorphism, 1093 MathlibAnnex.CStarAlgebra.twoSidedPointwiseLimit_symm_apply] 1094 exact MathlibAnnex.CStarAlgebra.tendsto_pointwiseLimit 1095 (fun n => (rightAutomorphisms 1096 rho hrho sigma hsigma xi eta hxi heta n).symm) 1097 (rightAutomorphisms_symm_cauchy 1098 rho hrho sigma hsigma xi eta hxi heta) a 1099 have hleft (b : Limit) : Tendsto (fun n => 1100 leftAutomorphisms rho hrho sigma hsigma xi eta hxi heta (n + 1) b) 1101 atTop (nhds (leftLimitAutomorphism 1102 rho hrho sigma hsigma xi eta hxi heta b)) := by 1103 apply (tendsto_add_atTop_iff_nat 1104 (f := fun n => leftAutomorphisms 1105 rho hrho sigma hsigma xi eta hxi heta n b) 1).2 1106 simpa [leftLimitAutomorphism, 1107 MathlibAnnex.CStarAlgebra.twoSidedPointwiseLimit_apply, 1108 MathlibAnnex.CStarAlgebra.pointwiseLimitHom_apply] using 1109 MathlibAnnex.CStarAlgebra.tendsto_pointwiseLimit 1110 (leftAutomorphisms rho hrho sigma hsigma xi eta hxi heta) 1111 (leftAutomorphisms_cauchy 1112 rho hrho sigma hsigma xi eta hxi heta) b 1113 have hcomp := MathlibAnnex.Metric.tendsto_comp_of_isometry 1114 (fun n => leftAutomorphisms 1115 rho hrho sigma hsigma xi eta hxi heta (n + 1)) 1116 (fun n => (rightAutomorphisms 1117 rho hrho sigma hsigma xi eta hxi heta n).symm a) 1118 (fun n => StarAlgEquiv.isometry 1119 (leftAutomorphisms rho hrho sigma hsigma xi eta hxi heta (n + 1))) 1120 hright (hleft ((rightLimitAutomorphism 1121 rho hrho sigma hsigma xi eta hxi heta).symm a)) 1122 simpa [outputAutomorphisms_eq, asymptoticAutomorphism] using hcomp 1123 1124theorem tendsto_implementingAutomorphism (a : Limit) : 1125 Tendsto (fun t : ℝ => 1126 implementingAutomorphism rho hrho sigma hsigma xi eta hxi heta t a) 1127 atTop (nhds (asymptoticAutomorphism 1128 rho hrho sigma hsigma xi eta hxi heta a)) := by 1129 have hcomp := MathlibAnnex.Metric.tendsto_comp_of_isometry 1130 (fun t => innerAt 1131 (leftContinuousPath rho hrho sigma hsigma xi eta hxi heta t)) 1132 (fun t => (innerAt 1133 (rightContinuousPath rho hrho sigma hsigma xi eta hxi heta t)).symm a) 1134 (fun t => StarAlgEquiv.isometry 1135 (innerAt (leftContinuousPath rho hrho sigma hsigma xi eta hxi heta t))) 1136 (tendsto_rightContinuousPath_inverse 1137 rho hrho sigma hsigma xi eta hxi heta a) 1138 (tendsto_leftContinuousPath_forward rho hrho sigma hsigma xi eta hxi heta 1139 ((rightLimitAutomorphism rho hrho sigma hsigma xi eta hxi heta).symm a)) 1140 simpa [implementingAutomorphism_eq, asymptoticAutomorphism] using hcomp 1141 1142theorem tendsto_implementingAutomorphism_symm (a : Limit) : 1143 Tendsto (fun t : ℝ => 1144 (implementingAutomorphism rho hrho sigma hsigma xi eta hxi heta t).symm a) 1145 atTop (nhds ((asymptoticAutomorphism 1146 rho hrho sigma hsigma xi eta hxi heta).symm a)) := by 1147 have hcomp := MathlibAnnex.Metric.tendsto_comp_of_isometry 1148 (fun t => innerAt 1149 (rightContinuousPath rho hrho sigma hsigma xi eta hxi heta t)) 1150 (fun t => (innerAt 1151 (leftContinuousPath rho hrho sigma hsigma xi eta hxi heta t)).symm a) 1152 (fun t => StarAlgEquiv.isometry 1153 (innerAt (rightContinuousPath rho hrho sigma hsigma xi eta hxi heta t))) 1154 (tendsto_leftContinuousPath_inverse 1155 rho hrho sigma hsigma xi eta hxi heta a) 1156 (tendsto_rightContinuousPath_forward rho hrho sigma hsigma xi eta hxi heta 1157 ((leftLimitAutomorphism rho hrho sigma hsigma xi eta hxi heta).symm a)) 1158 simpa [implementingAutomorphism_symm_eq, asymptoticAutomorphism] using hcomp 1159 1160theorem asymptoticAutomorphism_state (a : Limit) : 1161 Representation.vectorFunctional rho xi 1162 (asymptoticAutomorphism rho hrho sigma hsigma xi eta hxi heta a) = 1163 Representation.vectorFunctional sigma eta a := by 1164 apply tendsto_nhds_unique 1165 ((Representation.vectorFunctional rho xi).continuous.tendsto _ |>.comp 1166 (tendsto_outputAutomorphisms_asymptoticAutomorphism 1167 rho hrho sigma hsigma xi eta hxi heta a)) 1168 exact tendsto_outputAutomorphisms_state 1169 rho hrho sigma hsigma xi eta hxi heta a 1170 1171include hrho hsigma hxi heta in 1172theorem asymptoticallyInner_vectorFunctional : 1173 ∃ alpha : StarAlgEquiv ℂ Limit Limit, ∃ U : ℝ → unitary Limit, 1174 Continuous U ∧ U 0 = 1 ∧ 1175 (∀ a, Representation.vectorFunctional rho xi (alpha a) = 1176 Representation.vectorFunctional sigma eta a) ∧ 1177 (∀ a, Tendsto (fun t => Unitary.conjStarAlgAut ℂ Limit (U t) a) 1178 atTop (nhds (alpha a))) ∧ 1179 ∀ a, Tendsto (fun t => 1180 (Unitary.conjStarAlgAut ℂ Limit (U t)).symm a) 1181 atTop (nhds (alpha.symm a)) := by 1182 exact ⟨asymptoticAutomorphism rho hrho sigma hsigma xi eta hxi heta, 1183 implementingUnitary rho hrho sigma hsigma xi eta hxi heta, 1184 continuous_implementingUnitary rho hrho sigma hsigma xi eta hxi heta, 1185 implementingUnitary_zero rho hrho sigma hsigma xi eta hxi heta, 1186 asymptoticAutomorphism_state rho hrho sigma hsigma xi eta hxi heta, 1187 tendsto_implementingAutomorphism rho hrho sigma hsigma xi eta hxi heta, 1188 tendsto_implementingAutomorphism_symm rho hrho sigma hsigma xi eta hxi heta⟩ 1189 1190include hrho hsigma hxi heta in 1191theorem hasInnerIntertwiningSequence_vectorFunctional : 1192 HasInnerIntertwiningSequence 1193 (Representation.vectorFunctional rho xi) 1194 (Representation.vectorFunctional sigma eta) := by 1195 refine ⟨outputAutomorphisms rho hrho sigma hsigma xi eta hxi heta, 1196 outputAutomorphisms_cauchy rho hrho sigma hsigma xi eta hxi heta, 1197 outputAutomorphisms_symm_cauchy rho hrho sigma hsigma xi eta hxi heta, 1198 ?_, tendsto_outputAutomorphisms_state rho hrho sigma hsigma xi eta hxi heta⟩ 1199 intro n 1200 exact ⟨outputUnitary rho hrho sigma hsigma xi eta hxi heta n, rfl⟩ 1201 1202end Sequences 1203 1204set_option maxHeartbeats 1600000 in 1205/-- Every pair of pure CAR states has a genuine two-sided inner 1206intertwining sequence. -/ 1207theorem hasInnerIntertwiningSequence_of_pure 1208 (phi psi : Limit →L[ℂ] ℂ) 1209 (hphi : MathlibAnnex.CStarAlgebra.IsPureState Limit phi) (hpsi : MathlibAnnex.CStarAlgebra.IsPureState Limit psi) : 1210 HasInnerIntertwiningSequence phi psi := by 1211 have hphiState : phi ∈ stateSpace Limit := extremePoints_subset hphi 1212 let fphi := positiveLinearMapOfMemStateSpace phi hphiState 1213 let rho : Representation Limit fphi.GNS := fphi.gnsStarAlgHom 1214 let xi : fphi.GNS := fphi.gnsCyclicVector 1215 have hxi : ‖xi‖ = 1 := by 1216 change ‖stateGNSVector phi hphiState‖ = 1 1217 exact norm_stateGNSVector phi hphiState 1218 letI : Nontrivial fphi.GNS := by 1219 apply nontrivial_of_ne xi 0 1220 intro hzero 1221 have hnorm := congrArg norm hzero 1222 rw [hxi, norm_zero] at hnorm 1223 norm_num at hnorm 1224 have hrho : StarAlgHom.IsIrreducible rho := by 1225 simpa [rho, fphi] using 1226 isIrreducible_pureState_gnsStarAlgHom phi hphiState hphi 1227 have hphiVF : Representation.vectorFunctional rho xi = phi := by 1228 apply ContinuousLinearMap.ext 1229 intro a 1230 rw [Representation.vectorFunctional_apply] 1231 change inner ℂ (stateGNSVector phi hphiState) 1232 ((positiveLinearMapOfMemStateSpace phi hphiState).gnsStarAlgHom a 1233 (stateGNSVector phi hphiState)) = phi a 1234 exact inner_gnsStarAlgHom_stateGNSVector phi hphiState a 1235 have hpsiState : psi ∈ stateSpace Limit := extremePoints_subset hpsi 1236 let fpsi := positiveLinearMapOfMemStateSpace psi hpsiState 1237 let sigma : Representation Limit fpsi.GNS := fpsi.gnsStarAlgHom 1238 let eta : fpsi.GNS := fpsi.gnsCyclicVector 1239 have heta : ‖eta‖ = 1 := by 1240 change ‖stateGNSVector psi hpsiState‖ = 1 1241 exact norm_stateGNSVector psi hpsiState 1242 letI : Nontrivial fpsi.GNS := by 1243 apply nontrivial_of_ne eta 0 1244 intro hzero 1245 have hnorm := congrArg norm hzero 1246 rw [heta, norm_zero] at hnorm 1247 norm_num at hnorm 1248 have hsigma : StarAlgHom.IsIrreducible sigma := by 1249 simpa [sigma, fpsi] using 1250 isIrreducible_pureState_gnsStarAlgHom psi hpsiState hpsi 1251 have hpsiVF : Representation.vectorFunctional sigma eta = psi := by 1252 apply ContinuousLinearMap.ext 1253 intro a 1254 rw [Representation.vectorFunctional_apply] 1255 change inner ℂ (stateGNSVector psi hpsiState) 1256 ((positiveLinearMapOfMemStateSpace psi hpsiState).gnsStarAlgHom a 1257 (stateGNSVector psi hpsiState)) = psi a 1258 exact inner_gnsStarAlgHom_stateGNSVector psi hpsiState a 1259 rw [← hphiVF, ← hpsiVF] 1260 exact hasInnerIntertwiningSequence_vectorFunctional 1261 rho hrho sigma hsigma xi eta hxi heta 1262 1263set_option maxHeartbeats 1600000 in 1264/-- Every pair of pure CAR states is connected by one norm-continuous 1265unitary path whose inner automorphisms, and their actual inverses, converge 1266point-norm to the transporting automorphism and its inverse. -/ 1267theorem asymptoticallyInnerPureStateHomogeneity : AsymptoticallyInnerPureStateHomogeneity := by 1268 intro phi psi hphi hpsi 1269 have hphiState : phi ∈ stateSpace Limit := extremePoints_subset hphi 1270 let fphi := positiveLinearMapOfMemStateSpace phi hphiState 1271 let rho : Representation Limit fphi.GNS := fphi.gnsStarAlgHom 1272 let xi : fphi.GNS := fphi.gnsCyclicVector 1273 have hxi : ‖xi‖ = 1 := by 1274 change ‖stateGNSVector phi hphiState‖ = 1 1275 exact norm_stateGNSVector phi hphiState 1276 letI : Nontrivial fphi.GNS := by 1277 apply nontrivial_of_ne xi 0 1278 intro hzero 1279 have hnorm := congrArg norm hzero 1280 rw [hxi, norm_zero] at hnorm 1281 norm_num at hnorm 1282 have hrho : StarAlgHom.IsIrreducible rho := by 1283 simpa [rho, fphi] using 1284 isIrreducible_pureState_gnsStarAlgHom phi hphiState hphi 1285 have hphiVF : Representation.vectorFunctional rho xi = phi := by 1286 apply ContinuousLinearMap.ext 1287 intro a 1288 rw [Representation.vectorFunctional_apply] 1289 change inner ℂ (stateGNSVector phi hphiState) 1290 ((positiveLinearMapOfMemStateSpace phi hphiState).gnsStarAlgHom a 1291 (stateGNSVector phi hphiState)) = phi a 1292 exact inner_gnsStarAlgHom_stateGNSVector phi hphiState a 1293 have hpsiState : psi ∈ stateSpace Limit := extremePoints_subset hpsi 1294 let fpsi := positiveLinearMapOfMemStateSpace psi hpsiState 1295 let sigma : Representation Limit fpsi.GNS := fpsi.gnsStarAlgHom 1296 let eta : fpsi.GNS := fpsi.gnsCyclicVector 1297 have heta : ‖eta‖ = 1 := by 1298 change ‖stateGNSVector psi hpsiState‖ = 1 1299 exact norm_stateGNSVector psi hpsiState 1300 letI : Nontrivial fpsi.GNS := by 1301 apply nontrivial_of_ne eta 0 1302 intro hzero 1303 have hnorm := congrArg norm hzero 1304 rw [heta, norm_zero] at hnorm 1305 norm_num at hnorm 1306 have hsigma : StarAlgHom.IsIrreducible sigma := by 1307 simpa [sigma, fpsi] using 1308 isIrreducible_pureState_gnsStarAlgHom psi hpsiState hpsi 1309 have hpsiVF : Representation.vectorFunctional sigma eta = psi := by 1310 apply ContinuousLinearMap.ext 1311 intro a 1312 rw [Representation.vectorFunctional_apply] 1313 change inner ℂ (stateGNSVector psi hpsiState) 1314 ((positiveLinearMapOfMemStateSpace psi hpsiState).gnsStarAlgHom a 1315 (stateGNSVector psi hpsiState)) = psi a 1316 exact inner_gnsStarAlgHom_stateGNSVector psi hpsiState a 1317 obtain ⟨alpha, U, hU, hU0, hstate, hforward, hinverse⟩ := 1318 asymptoticallyInner_vectorFunctional 1319 rho hrho sigma hsigma xi eta hxi heta 1320 refine ⟨alpha, U, hU, hU0, ?_, hforward, hinverse⟩ 1321 intro a 1322 rw [← hphiVF, ← hpsiVF] 1323 exact hstate a 1324 1325/-- Regression adapter: forgetting the implementing path recovers the 1326previous CAR approximate-inner homogeneity statement. -/ 1327theorem homogeneity_from_asymptotic : PureStateHomogeneity := 1328 homogeneity_of_asymptoticallyInner asymptoticallyInnerPureStateHomogeneity 1329 1330/-- The CAR homogeneity endpoint, with the intertwining supplier discharged. -/ 1331theorem homogeneity : PureStateHomogeneity := 1332 homogeneity_of_innerIntertwiningSequences 1333 (fun phi psi hphi hpsi => 1334 hasInnerIntertwiningSequence_of_pure phi psi hphi hpsi) 1335 1336end MathlibAnnex.CStarAlgebra.CAR