Exact source: MathlibAnnex/Analysis/CStarAlgebra/CAR/GlobalTransport.lean
Pinned GitHub source · Raw UTF-8 source
Back to Approximately inner homogeneity of pure CAR states · Back to Pure-state homogeneity of the completed CAR algebra · Back to Choosing the CAR shell family from proved homogeneity
1import MathlibAnnex.Analysis.CStarAlgebra.DenseCauchy2import MathlibAnnex.Topology.InfinitePath3import Mathlib.Topology.Algebra.Star.Unitary4import MathlibAnnex.Analysis.CStarAlgebra.CAR.Homogeneity5import MathlibAnnex.Analysis.CStarAlgebra.CAR.StateTransport67/-!8# Alternating global transport for CAR pure states910The local test order is encoded in `AlternatingState`: its movement function11has already consumed the current stage-test closeness. A transition first12moves the left vector close on the right tests, then moves the right vector13close on the next left tests. Thus no future test set is chosen after the14hypothesis which has to control it.15-/1617set_option autoImplicit false1819noncomputable section2021open Filter MathlibAnnex.Analysis.CStarAlgebra TopologicalSpace2223namespace MathlibAnnex.CStarAlgebra.CAR2425noncomputable def transportDense : ℕ → Limit := denseSeq Limit2627theorem denseRange_transportDense : DenseRange transportDense :=28 denseRange_denseSeq Limit2930noncomputable def densePrefix (n : ℕ) : Finset Limit :=31 by classical exact (Finset.range (n + 1)).image transportDense3233noncomputable def innerAt (u : unitary Limit) : StarAlgEquiv ℂ Limit Limit :=34 Unitary.conjStarAlgAut ℂ Limit (star u)3536noncomputable def protectedPrefix (u : unitary Limit) (n : ℕ) : Finset Limit :=37 by classical exact densePrefix n ∪ (densePrefix n).image (innerAt u).symm3839noncomputable def stageTests (n : ℕ) : Finset Limit :=40 by41 classical42 exact (Finset.univ.product Finset.univ).image43 (fun ij : Fin (2 ^ n) × Fin (2 ^ n) => limitMatrixUnit n ij.1 ij.2)4445def transportBudget (n : ℕ) : ℝ := (1 / 2 : ℝ) ^ n4647theorem transportBudget_pos (n : ℕ) : 0 < transportBudget n := by48 norm_num [transportBudget]4950theorem summable_transportBudget : Summable transportBudget := by51 change Summable fun n : ℕ => (1 / 2 : ℝ) ^ n52 exact summable_geometric_of_norm_lt_one (by norm_num)5354theorem mem_densePrefix {j n : ℕ} (hjn : j ≤ n) :55 transportDense j ∈ densePrefix n := by56 classical57 simp only [densePrefix]58 apply Finset.mem_image.mpr59 exact ⟨j, Finset.mem_range.mpr (Nat.lt_succ_of_le hjn), rfl⟩6061theorem mem_protectedPrefix {u : unitary Limit} {j n : ℕ} (hjn : j ≤ n) :62 transportDense j ∈ protectedPrefix u n :=63 by64 classical65 exact Finset.mem_union_left _ (mem_densePrefix hjn)6667theorem mem_symm_protectedPrefix {u : unitary Limit} {j n : ℕ} (hjn : j ≤ n) :68 (innerAt u).symm (transportDense j) ∈ protectedPrefix u n := by69 classical70 simp only [protectedPrefix]71 apply Finset.mem_union_right72 apply Finset.mem_image.mpr73 exact ⟨transportDense j, mem_densePrefix hjn, rfl⟩7475theorem mem_stageTests (n : ℕ) (i j : Fin (2 ^ n)) :76 limitMatrixUnit n i j ∈ stageTests n := by77 classical78 simp only [stageTests]79 apply Finset.mem_image.mpr80 exact ⟨(i, j), Finset.mem_product.mpr ⟨Finset.mem_univ _, Finset.mem_univ _⟩, rfl⟩8182/-- A recursion state whose left local theorem has already been specialized83to the current right vector. -/84structure AlternatingState85 {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 : ℕ) where92 left : unitary Limit93 right : unitary Limit94 leftPath : Path 1 left95 rightPath : Path 1 right96 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 rho104 (rho (u : Limit) (rho (left : Limit) xi)) a -105 Representation.vectorFunctional sigma (sigma (right : Limit) eta) a‖ < epsilon'106107/-- A transition records both small corrections and the state estimate at108the left midpoint, before the right correction is applied. -/109structure AlternatingTransition110 {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) where118 leftCorrection : unitary Limit119 rightCorrection : unitary Limit120 leftCorrectionPath : Path 1 leftCorrection121 rightCorrectionPath : Path 1 rightCorrection122 next : AlternatingState rho sigma xi eta (step + 1)123 next_left : next.left = leftCorrection * s.left124 next_right : next.right = rightCorrection * s.right125 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 step130 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 step135 state_small : ∀ j, j ≤ step →136 ‖Representation.vectorFunctional rho137 (rho (next.left : Limit) xi) ((innerAt s.right).symm (transportDense j)) -138 Representation.vectorFunctional sigma139 (sigma (s.right : Limit) eta) ((innerAt s.right).symm (transportDense j))‖ <140 transportBudget step141142set_option maxHeartbeats 1600000 in143theorem nonempty_transition144 {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) := by154 classical155 have hleftUnit : ‖rho (s.left : Limit) xi‖ = 1 := by156 rw [(rho (s.left : Limit)).norm_map_of_mem_unitary157 (Unitary.map_mem rho s.left.property), hxi]158 have hrightUnit : ‖sigma (s.right : Limit) eta‖ = 1 := by159 rw [(sigma (s.right : Limit)).norm_map_of_mem_unitary160 (Unitary.map_mem sigma s.right.property), heta]161 obtain ⟨nb, db, hdb, hB⟩ :=162 exists_stageTests_crossRepresentation_path_approx sigma hsigma163 (protectedPrefix s.right step) (transportBudget_pos step)164 let requestLeft : Finset Limit :=165 stageTests nb ∪ (densePrefix step).image (innerAt s.right).symm166 have hmin : 0 < min db (transportBudget step) := lt_min hdb (transportBudget_pos step)167 obtain ⟨u, pu, husmall, huapprox⟩ := s.move requestLeft _ hmin168 let left' : unitary Limit := u * s.left169 let leftSegment : Path s.left left' :=170 { toFun := fun t => pu t * s.left171 continuous_toFun := by fun_prop172 source' := by rw [pu.source]; simp173 target' := by rw [pu.target] }174 let leftPath' : Path 1 left' := s.leftPath.trans leftSegment175 have hleft'Unit : ‖rho (left' : Limit) xi‖ = 1 := by176 rw [(rho (left' : Limit)).norm_map_of_mem_unitary177 (Unitary.map_mem rho left'.property), hxi]178 obtain ⟨na, da, hda, hA⟩ :=179 exists_stageTests_crossRepresentation_path_approx rho hrho180 (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 := by186 intro i j187 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 := by191 change rho (u : Limit) (rho (s.left : Limit) xi) =192 rho ((u : Limit) * (s.left : Limit)) xi193 rw [map_mul, mul_apply_eq_comp]194 rw [hsimp, norm_sub_rev] at h195 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 hda199 let right' : unitary Limit := v * s.right200 let rightSegment : Path s.right right' :=201 { toFun := fun t => pv t * s.right202 continuous_toFun := by fun_prop203 source' := by rw [pv.source]; simp204 target' := by rw [pv.target] }205 let rightPath' : Path 1 right' := s.rightPath.trans rightSegment206 have hright'Unit : ‖sigma (right' : Limit) eta‖ = 1 := by207 rw [(sigma (right' : Limit)).norm_map_of_mem_unitary208 (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 := by214 intro i j215 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 := by218 change sigma (v : Limit) (sigma (s.right : Limit) eta) =219 sigma ((v : Limit) * (s.right : Limit)) eta220 rw [map_mul, mul_apply_eq_comp]221 rw [hsimp, norm_sub_rev] at h222 exact h223 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 := u232 rightCorrection := v233 leftCorrectionPath := pu234 rightCorrectionPath := pv235 next := next236 next_left := rfl237 next_right := rfl238 left_small := husmall239 right_small := hvsmall240 state_small := ?_ }⟩241 intro j hj242 have h := huapprox ((innerAt s.right).symm (transportDense j))243 (Finset.mem_union_right _ (Finset.mem_image.mpr244 ⟨transportDense j, mem_densePrefix hj, rfl⟩))245 have hsimp : rho (u : Limit) (rho (s.left : Limit) xi) =246 rho (next.left : Limit) xi := by247 change rho (u : Limit) (rho (s.left : Limit) xi) =248 rho ((u : Limit) * (s.left : Limit)) xi249 rw [map_mul, mul_apply_eq_comp]250 rw [hsimp] at h251 exact lt_of_lt_of_le h (min_le_right _ _)252253set_option maxHeartbeats 1600000 in254theorem nonempty_initialState255 {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) := by264 classical265 obtain ⟨nb, db, hdb, hB⟩ :=266 exists_stageTests_crossRepresentation_path_approx sigma hsigma267 (protectedPrefix 1 0) (transportBudget_pos 0)268 obtain ⟨u, pu, hu⟩ := exists_unitary_crossRepresentation_path_approx269 rho hrho sigma xi eta hxi heta (stageTests nb) hdb270 let left' : unitary Limit := u271 have hleft'Unit : ‖rho (left' : Limit) xi‖ = 1 := by272 rw [(rho (left' : Limit)).norm_map_of_mem_unitary273 (Unitary.map_mem rho left'.property), hxi]274 obtain ⟨na, da, hda, hA⟩ :=275 exists_stageTests_crossRepresentation_path_approx rho hrho276 (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 := by281 intro i j282 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)‖ < db286 rw [norm_sub_rev]287 exact h288 obtain ⟨v, pv, _hvsmall, hvapprox⟩ :=289 hB rho eta (rho (left' : Limit) xi) heta hleft'Unit hBclose290 (stageTests na) da hda291 let right' : unitary Limit := v292 have hright'Unit : ‖sigma (right' : Limit) eta‖ = 1 := by293 rw [(sigma (right' : Limit)).norm_map_of_mem_unitary294 (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 := by300 intro i j301 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)‖ < da306 rw [norm_sub_rev]307 exact h308 exact ⟨{309 left := left'310 right := right'311 leftPath := pu312 rightPath := pv313 move := hA sigma (rho (left' : Limit) xi) (sigma (right' : Limit) eta)314 hleft'Unit hright'Unit hAclose }⟩315316noncomputable def initialState317 {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)327328noncomputable def chosenTransition329 {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)340341noncomputable def alternatingStates342 {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 n351 | 0 => initialState rho hrho sigma hsigma xi eta hxi heta352 | n + 1 => (chosenTransition rho hrho sigma hsigma xi eta hxi heta353 (alternatingStates rho hrho sigma hsigma xi eta hxi heta n)).next354355noncomputable def alternatingTransitions356 {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 eta366 (alternatingStates rho hrho sigma hsigma xi eta hxi heta n) :=367 chosenTransition rho hrho sigma hsigma xi eta hxi heta368 (alternatingStates rho hrho sigma hsigma xi eta hxi heta n)369370section Sequences371372variable {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)380381local notation "S" => alternatingStates rho hrho sigma hsigma xi eta hxi heta382local notation "T" => alternatingTransitions rho hrho sigma hsigma xi eta hxi heta383384/-- Integer-time vertices of the left concatenated path. Negative times are385constant, time zero is the unit, and time `n+1` is the `n`th recursion state. -/386noncomputable def leftPathPoints : ℤ → unitary Limit387 | .ofNat 0 => 1388 | .ofNat (n + 1) => (S n).left389 | .negSucc _ => 1390391/-- Integer-time vertices of the right concatenated path. -/392noncomputable def rightPathPoints : ℤ → unitary Limit393 | .ofNat 0 => 1394 | .ofNat (n + 1) => (S n).right395 | .negSucc _ => 1396397/-- A correction path, translated on the right by the previous accumulated398unitary. -/399def translatedCorrectionPath {u w : unitary Limit} (p : Path 1 u) :400 Path w (u * w) :=401 { toFun := fun t => p t * w402 continuous_toFun := by fun_prop403 source' := by rw [p.source]; simp404 target' := by rw [p.target] }405406/-- Unit-interval pieces of the left unbounded path. -/407noncomputable def leftPathSegments :408 (z : ℤ) → Path409 (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).leftPath412 | .ofNat (n + 1) => by413 let q : Path (S n).left ((T n).leftCorrection * (S n).left) :=414 translatedCorrectionPath (w := (S n).left) (T n).leftCorrectionPath415 exact q.cast (by simp [leftPathPoints]) (by416 simp only [leftPathPoints]417 change (S (n + 1)).left = (T n).leftCorrection * (S n).left418 exact (T n).next_left)419 | .negSucc n => by420 have hz : Int.negSucc n + 1 =421 match n with422 | 0 => (0 : ℤ)423 | k + 1 => Int.negSucc k := by424 cases n <;> simp [Int.negSucc_eq]425 rw [hz]426 cases n <;> exact Path.refl _427428/-- Unit-interval pieces of the right unbounded path. -/429noncomputable def rightPathSegments :430 (z : ℤ) → Path431 (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).rightPath434 | .ofNat (n + 1) => by435 let q : Path (S n).right ((T n).rightCorrection * (S n).right) :=436 translatedCorrectionPath (w := (S n).right) (T n).rightCorrectionPath437 exact q.cast (by simp [rightPathPoints]) (by438 simp only [rightPathPoints]439 change (S (n + 1)).right = (T n).rightCorrection * (S n).right440 exact (T n).next_right)441 | .negSucc n => by442 have hz : Int.negSucc n + 1 =443 match n with444 | 0 => (0 : ℤ)445 | k + 1 => Int.negSucc k := by446 cases n <;> simp [Int.negSucc_eq]447 rw [hz]448 cases n <;> exact Path.refl _449450/-- The left locally finite concatenation, constant at negative times. -/451noncomputable def leftContinuousPath (t : ℝ) : unitary Limit :=452 MathlibAnnex.Path.infiniteConcat453 (leftPathPoints rho hrho sigma hsigma xi eta hxi heta)454 (leftPathSegments rho hrho sigma hsigma xi eta hxi heta) t455456/-- The right locally finite concatenation, constant at negative times. -/457noncomputable def rightContinuousPath (t : ℝ) : unitary Limit :=458 MathlibAnnex.Path.infiniteConcat459 (rightPathPoints rho hrho sigma hsigma xi eta hxi heta)460 (rightPathSegments rho hrho sigma hsigma xi eta hxi heta) t461462theorem continuous_leftContinuousPath :463 Continuous (leftContinuousPath rho hrho sigma hsigma xi eta hxi heta) :=464 MathlibAnnex.Path.continuous_infiniteConcat _ _465466theorem continuous_rightContinuousPath :467 Continuous (rightContinuousPath rho hrho sigma hsigma xi eta hxi heta) :=468 MathlibAnnex.Path.continuous_infiniteConcat _ _469470theorem leftContinuousPath_zero :471 leftContinuousPath rho hrho sigma hsigma xi eta hxi heta 0 = 1 := by472 rw [leftContinuousPath, MathlibAnnex.Path.infiniteConcat, Int.floor_zero]473 change (S 0).leftPath474 ⟨Int.fract (0 : ℝ), unitInterval.fract_mem (0 : ℝ)⟩ = 1475 rw [show (⟨Int.fract (0 : ℝ), unitInterval.fract_mem (0 : ℝ)⟩ :476 unitInterval) = 0 by ext; norm_num [Int.fract]]477 exact (S 0).leftPath.source478479theorem rightContinuousPath_zero :480 rightContinuousPath rho hrho sigma hsigma xi eta hxi heta 0 = 1 := by481 rw [rightContinuousPath, MathlibAnnex.Path.infiniteConcat, Int.floor_zero]482 change (S 0).rightPath483 ⟨Int.fract (0 : ℝ), unitInterval.fract_mem (0 : ℝ)⟩ = 1484 rw [show (⟨Int.fract (0 : ℝ), unitInterval.fract_mem (0 : ℝ)⟩ :485 unitInterval) = 0 by ext; norm_num [Int.fract]]486 exact (S 0).rightPath.source487488theorem 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).leftCorrectionPath492 ⟨(t : ℝ) - (n + 1), by493 constructor494 · exact sub_nonneg.mpr (by simpa using t.property.1)495 · apply (sub_le_iff_le_add).mpr496 have ht := t.property.2497 linarith⟩ *498 (S n).left := by499 let tz : Set.Icc ((Int.ofNat (n + 1) : ℤ) : ℝ)500 ((Int.ofNat (n + 1) : ℤ) + 1 : ℝ) :=501 ⟨t, by502 constructor503 · simpa using t.property.1504 · have ht := t.property.2505 norm_num at ht ⊢506 linarith⟩507 have h := MathlibAnnex.Path.infiniteConcat_eq_intervalPath508 (leftPathPoints rho hrho sigma hsigma xi eta hxi heta)509 (leftPathSegments rho hrho sigma hsigma xi eta hxi heta)510 (Int.ofNat (n + 1)) tz511 dsimp only [tz] at h512 convert h using 1 <;>513 simp [leftContinuousPath, MathlibAnnex.Path.intervalPath,514 leftPathSegments, translatedCorrectionPath, Path.cast]515 congr 2516517theorem 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).rightCorrectionPath521 ⟨(t : ℝ) - (n + 1), by522 constructor523 · exact sub_nonneg.mpr (by simpa using t.property.1)524 · apply (sub_le_iff_le_add).mpr525 have ht := t.property.2526 linarith⟩ *527 (S n).right := by528 let tz : Set.Icc ((Int.ofNat (n + 1) : ℤ) : ℝ)529 ((Int.ofNat (n + 1) : ℤ) + 1 : ℝ) :=530 ⟨t, by531 constructor532 · simpa using t.property.1533 · have ht := t.property.2534 norm_num at ht ⊢535 linarith⟩536 have h := MathlibAnnex.Path.infiniteConcat_eq_intervalPath537 (rightPathPoints rho hrho sigma hsigma xi eta hxi heta)538 (rightPathSegments rho hrho sigma hsigma xi eta hxi heta)539 (Int.ofNat (n + 1)) tz540 dsimp only [tz] at h541 convert h using 1 <;>542 simp [rightContinuousPath, MathlibAnnex.Path.intervalPath,543 rightPathSegments, translatedCorrectionPath, Path.cast]544 congr 2545546noncomputable def leftAutomorphisms (n : ℕ) : StarAlgEquiv ℂ Limit Limit :=547 innerAt (S n).left548549noncomputable def rightAutomorphisms (n : ℕ) : StarAlgEquiv ℂ Limit Limit :=550 innerAt (S n).right551552theorem 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 n557 (transportDense j)‖ ≤ transportBudget n := by558 let s : unitInterval :=559 ⟨(t : ℝ) - (n + 1), by560 constructor561 · exact sub_nonneg.mpr (by simpa using t.property.1)562 · apply (sub_le_iff_le_add).mpr563 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).left568 (star ((T n).leftCorrectionPath s : Limit) * transportDense j *569 ((T n).leftCorrectionPath s : Limit)) := by570 simp [innerAt, mul_assoc]571 rw [hformula, leftAutomorphisms]572 calc573 _ = ‖star ((T n).leftCorrectionPath s : Limit) * transportDense j *574 ((T n).leftCorrectionPath s : Limit) - transportDense j‖ := by575 have h := (StarAlgEquiv.isometry (innerAt (S n).left)).dist_eq576 (star ((T n).leftCorrectionPath s : Limit) * transportDense j *577 ((T n).leftCorrectionPath s : Limit)) (transportDense j)578 simpa only [dist_eq_norm] using h579 _ ≤ transportBudget n :=580 le_of_lt (((T n).left_small s _ (mem_protectedPrefix hj)).2)581582theorem 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)).symm585 (transportDense j) -586 (leftAutomorphisms rho hrho sigma hsigma xi eta hxi heta n).symm587 (transportDense j)‖ ≤ transportBudget n := by588 let s : unitInterval :=589 ⟨(t : ℝ) - (n + 1), by590 constructor591 · exact sub_nonneg.mpr (by simpa using t.property.1)592 · apply (sub_le_iff_le_add).mpr593 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)).symm597 (transportDense j) =598 ((T n).leftCorrectionPath s : Limit) *599 (innerAt (S n).left).symm (transportDense j) *600 star ((T n).leftCorrectionPath s : Limit) := by601 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_ring609 rw [hformula, leftAutomorphisms]610 exact le_of_lt (((T n).left_small s _ (mem_symm_protectedPrefix hj)).1)611612theorem 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 n617 (transportDense j)‖ ≤ transportBudget n := by618 let s : unitInterval :=619 ⟨(t : ℝ) - (n + 1), by620 constructor621 · exact sub_nonneg.mpr (by simpa using t.property.1)622 · apply (sub_le_iff_le_add).mpr623 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).right628 (star ((T n).rightCorrectionPath s : Limit) * transportDense j *629 ((T n).rightCorrectionPath s : Limit)) := by630 simp [innerAt, mul_assoc]631 rw [hformula, rightAutomorphisms]632 calc633 _ = ‖star ((T n).rightCorrectionPath s : Limit) * transportDense j *634 ((T n).rightCorrectionPath s : Limit) - transportDense j‖ := by635 have h := (StarAlgEquiv.isometry (innerAt (S n).right)).dist_eq636 (star ((T n).rightCorrectionPath s : Limit) * transportDense j *637 ((T n).rightCorrectionPath s : Limit)) (transportDense j)638 simpa only [dist_eq_norm] using h639 _ ≤ transportBudget n :=640 le_of_lt (((T n).right_small s _ (mem_protectedPrefix hj)).2)641642theorem 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)).symm645 (transportDense j) -646 (rightAutomorphisms rho hrho sigma hsigma xi eta hxi heta n).symm647 (transportDense j)‖ ≤ transportBudget n := by648 let s : unitInterval :=649 ⟨(t : ℝ) - (n + 1), by650 constructor651 · exact sub_nonneg.mpr (by simpa using t.property.1)652 · apply (sub_le_iff_le_add).mpr653 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)).symm657 (transportDense j) =658 ((T n).rightCorrectionPath s : Limit) *659 (innerAt (S n).right).symm (transportDense j) *660 star ((T n).rightCorrectionPath s : Limit) := by661 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_ring669 rw [hformula, rightAutomorphisms]670 exact le_of_lt (((T n).right_small s _ (mem_symm_protectedPrefix hj)).1)671672theorem 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 n676 (transportDense j)‖ ≤ transportBudget n := by677 let t := T n678 have hnext : S (n + 1) = t.next := rfl679 rw [leftAutomorphisms, leftAutomorphisms, hnext, t.next_left]680 have hformula :681 innerAt (t.leftCorrection * (S n).left) (transportDense j) =682 innerAt (S n).left683 (star (t.leftCorrection : Limit) * transportDense j *684 (t.leftCorrection : Limit)) := by685 simp [innerAt, mul_assoc]686 rw [hformula]687 calc688 _ = ‖star (t.leftCorrection : Limit) * transportDense j *689 (t.leftCorrection : Limit) - transportDense j‖ := by690 have h := (StarAlgEquiv.isometry (innerAt (S n).left)).dist_eq691 (star (t.leftCorrection : Limit) * transportDense j *692 (t.leftCorrection : Limit)) (transportDense j)693 simpa only [dist_eq_norm] using h694 _ ≤ transportBudget n := by695 have h := (t.left_small (1 : Set.Icc (0 : ℝ) 1) _696 (mem_protectedPrefix hj)).2697 simpa only [t.leftCorrectionPath.target] using le_of_lt h698699theorem leftAutomorphisms_symm_step (n j : ℕ) (hj : j ≤ n) :700 ‖(leftAutomorphisms rho hrho sigma hsigma xi eta hxi heta (n + 1)).symm701 (transportDense j) -702 (leftAutomorphisms rho hrho sigma hsigma xi eta hxi heta n).symm703 (transportDense j)‖ ≤ transportBudget n := by704 let t := T n705 have hnext : S (n + 1) = t.next := rfl706 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) := by712 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_ring719 rw [hformula]720 have h := (t.left_small (1 : Set.Icc (0 : ℝ) 1) _721 (mem_symm_protectedPrefix hj)).1722 simpa only [t.leftCorrectionPath.target] using le_of_lt h723724theorem 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 n728 (transportDense j)‖ ≤ transportBudget n := by729 let t := T n730 have hnext : S (n + 1) = t.next := rfl731 rw [rightAutomorphisms, rightAutomorphisms, hnext, t.next_right]732 have hformula :733 innerAt (t.rightCorrection * (S n).right) (transportDense j) =734 innerAt (S n).right735 (star (t.rightCorrection : Limit) * transportDense j *736 (t.rightCorrection : Limit)) := by737 simp [innerAt, mul_assoc]738 rw [hformula]739 calc740 _ = ‖star (t.rightCorrection : Limit) * transportDense j *741 (t.rightCorrection : Limit) - transportDense j‖ := by742 have h := (StarAlgEquiv.isometry (innerAt (S n).right)).dist_eq743 (star (t.rightCorrection : Limit) * transportDense j *744 (t.rightCorrection : Limit)) (transportDense j)745 simpa only [dist_eq_norm] using h746 _ ≤ transportBudget n := by747 have h := (t.right_small (1 : Set.Icc (0 : ℝ) 1) _748 (mem_protectedPrefix hj)).2749 simpa only [t.rightCorrectionPath.target] using le_of_lt h750751theorem rightAutomorphisms_symm_step (n j : ℕ) (hj : j ≤ n) :752 ‖(rightAutomorphisms rho hrho sigma hsigma xi eta hxi heta (n + 1)).symm753 (transportDense j) -754 (rightAutomorphisms rho hrho sigma hsigma xi eta hxi heta n).symm755 (transportDense j)‖ ≤ transportBudget n := by756 let t := T n757 have hnext : S (n + 1) = t.next := rfl758 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) := by764 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_ring771 rw [hformula]772 have h := (t.right_small (1 : Set.Icc (0 : ℝ) 1) _773 (mem_symm_protectedPrefix hj)).1774 simpa only [t.rightCorrectionPath.target] using le_of_lt h775776theorem 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_steps780 transportDense denseRange_transportDense781 (leftAutomorphisms rho hrho sigma hsigma xi eta hxi heta)782 transportBudget summable_transportBudget783 (leftAutomorphisms_step rho hrho sigma hsigma xi eta hxi heta)784785theorem 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_steps789 transportDense denseRange_transportDense790 (fun n => (leftAutomorphisms rho hrho sigma hsigma xi eta hxi heta n).symm)791 transportBudget summable_transportBudget792 (leftAutomorphisms_symm_step rho hrho sigma hsigma xi eta hxi heta)793794theorem 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_steps798 transportDense denseRange_transportDense799 (rightAutomorphisms rho hrho sigma hsigma xi eta hxi heta)800 transportBudget summable_transportBudget801 (rightAutomorphisms_step rho hrho sigma hsigma xi eta hxi heta)802803theorem 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_steps807 transportDense denseRange_transportDense808 (fun n => (rightAutomorphisms rho hrho sigma hsigma xi eta hxi heta n).symm)809 transportBudget summable_transportBudget810 (rightAutomorphisms_symm_step rho hrho sigma hsigma xi eta hxi heta)811812theorem tendsto_transportBudget_zero :813 Tendsto transportBudget atTop (nhds 0) := by814 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)816817/-- The two-sided pointwise limit of the accumulated left conjugations. -/818noncomputable def leftLimitAutomorphism : StarAlgEquiv ℂ Limit Limit :=819 MathlibAnnex.CStarAlgebra.twoSidedPointwiseLimit820 (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)823824/-- The two-sided pointwise limit of the accumulated right conjugations. -/825noncomputable def rightLimitAutomorphism : StarAlgEquiv ℂ Limit Limit :=826 MathlibAnnex.CStarAlgebra.twoSidedPointwiseLimit827 (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)830831theorem 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)) := by835 apply MathlibAnnex.Metric.tendsto_atTop_of_isometry_segment_approx836 transportDense denseRange_transportDense837 (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.isometry840 (leftAutomorphisms rho hrho sigma hsigma xi eta hxi heta n))841 (fun t => StarAlgEquiv.isometry842 (innerAt (leftContinuousPath rho hrho sigma hsigma xi eta hxi heta t)))843 transportBudget tendsto_transportBudget_zero844 (fun n j hj t => by845 simpa only [dist_eq_norm] using846 leftContinuousPath_forward_dense_segment847 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] using852 MathlibAnnex.CStarAlgebra.tendsto_pointwiseLimit853 (leftAutomorphisms rho hrho sigma hsigma xi eta hxi heta)854 (leftAutomorphisms_cauchy rho hrho sigma hsigma xi eta hxi heta) a855856theorem 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 ((leftLimitAutomorphism860 rho hrho sigma hsigma xi eta hxi heta).symm a)) := by861 apply MathlibAnnex.Metric.tendsto_atTop_of_isometry_segment_approx862 transportDense denseRange_transportDense863 (fun n a =>864 (leftAutomorphisms rho hrho sigma hsigma xi eta hxi heta n).symm a)865 (fun t => (innerAt866 (leftContinuousPath rho hrho sigma hsigma xi eta hxi heta t)).symm)867 (fun n => StarAlgEquiv.isometry868 (leftAutomorphisms rho hrho sigma hsigma xi eta hxi heta n).symm)869 (fun t => StarAlgEquiv.isometry870 (innerAt (leftContinuousPath rho hrho sigma hsigma xi eta hxi heta t)).symm)871 transportBudget tendsto_transportBudget_zero872 (fun n j hj t => by873 simpa only [dist_eq_norm] using874 leftContinuousPath_inverse_dense_segment875 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_pointwiseLimit880 (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) a882883theorem 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)) := by887 apply MathlibAnnex.Metric.tendsto_atTop_of_isometry_segment_approx888 transportDense denseRange_transportDense889 (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.isometry892 (rightAutomorphisms rho hrho sigma hsigma xi eta hxi heta n))893 (fun t => StarAlgEquiv.isometry894 (innerAt (rightContinuousPath rho hrho sigma hsigma xi eta hxi heta t)))895 transportBudget tendsto_transportBudget_zero896 (fun n j hj t => by897 simpa only [dist_eq_norm] using898 rightContinuousPath_forward_dense_segment899 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] using904 MathlibAnnex.CStarAlgebra.tendsto_pointwiseLimit905 (rightAutomorphisms rho hrho sigma hsigma xi eta hxi heta)906 (rightAutomorphisms_cauchy rho hrho sigma hsigma xi eta hxi heta) a907908theorem 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 ((rightLimitAutomorphism912 rho hrho sigma hsigma xi eta hxi heta).symm a)) := by913 apply MathlibAnnex.Metric.tendsto_atTop_of_isometry_segment_approx914 transportDense denseRange_transportDense915 (fun n a =>916 (rightAutomorphisms rho hrho sigma hsigma xi eta hxi heta n).symm a)917 (fun t => (innerAt918 (rightContinuousPath rho hrho sigma hsigma xi eta hxi heta t)).symm)919 (fun n => StarAlgEquiv.isometry920 (rightAutomorphisms rho hrho sigma hsigma xi eta hxi heta n).symm)921 (fun t => StarAlgEquiv.isometry922 (innerAt (rightContinuousPath rho hrho sigma hsigma xi eta hxi heta t)).symm)923 transportBudget tendsto_transportBudget_zero924 (fun n j hj t => by925 simpa only [dist_eq_norm] using926 rightContinuousPath_inverse_dense_segment927 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_pointwiseLimit932 (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) a934935noncomputable def outputUnitary (n : ℕ) : unitary Limit :=936 star (S (n + 1)).left * (S n).right937938noncomputable def outputAutomorphisms (n : ℕ) : StarAlgEquiv ℂ Limit Limit :=939 Unitary.conjStarAlgAut ℂ Limit940 (outputUnitary rho hrho sigma hsigma xi eta hxi heta n)941942theorem 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.trans945 (leftAutomorphisms rho hrho sigma hsigma xi eta hxi heta (n + 1)) := by946 ext a947 simp [outputAutomorphisms, outputUnitary, rightAutomorphisms,948 leftAutomorphisms, innerAt, mul_assoc]949950theorem leftAutomorphisms_succ_cauchy :951 ∀ a, CauchySeq (fun n =>952 leftAutomorphisms rho hrho sigma hsigma xi eta hxi heta (n + 1) a) := by953 intro a954 exact (cauchySeq_shift 1).2955 (leftAutomorphisms_cauchy rho hrho sigma hsigma xi eta hxi heta a)956957theorem leftAutomorphisms_succ_symm_cauchy :958 ∀ a, CauchySeq (fun n =>959 (leftAutomorphisms rho hrho sigma hsigma xi eta hxi heta (n + 1)).symm a) := by960 intro a961 exact (cauchySeq_shift 1).2962 (leftAutomorphisms_symm_cauchy rho hrho sigma hsigma xi eta hxi heta a)963964theorem outputAutomorphisms_cauchy :965 ∀ a, CauchySeq (fun n =>966 outputAutomorphisms rho hrho sigma hsigma xi eta hxi heta n a) := by967 intro a968 have h := MathlibAnnex.CStarAlgebra.cauchySeq_trans_of_isometry969 (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) a973 simpa only [outputAutomorphisms_eq] using h974975theorem outputAutomorphisms_symm_cauchy :976 ∀ a, CauchySeq (fun n =>977 (outputAutomorphisms rho hrho sigma hsigma xi eta hxi heta n).symm a) := by978 intro a979 have h := MathlibAnnex.CStarAlgebra.cauchySeq_trans_of_isometry980 (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) a985 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.trans988 (rightAutomorphisms rho hrho sigma hsigma xi eta hxi heta n) := by989 intro n990 rw [outputAutomorphisms_eq]991 rfl992 simpa only [heq] using h993994theorem outputAutomorphisms_state_dense (n j : ℕ) (hj : j ≤ n) :995 ‖Representation.vectorFunctional rho xi996 (outputAutomorphisms rho hrho sigma hsigma xi eta hxi heta n997 (transportDense j)) -998 Representation.vectorFunctional sigma eta (transportDense j)‖ <999 transportBudget n := by1000 let t := T n1001 have hnext : S (n + 1) = t.next := rfl1002 have h := t.state_small j hj1003 rw [← hnext] at h1004 rw [Representation.vectorFunctional_map_apply,1005 Representation.vectorFunctional_map_apply] at h1006 have h' :1007 ‖Representation.vectorFunctional rho xi1008 (innerAt (S (n + 1)).left1009 ((innerAt (S n).right).symm (transportDense j))) -1010 Representation.vectorFunctional sigma eta1011 (innerAt (S n).right1012 ((innerAt (S n).right).symm (transportDense j)))‖ <1013 transportBudget n := by1014 simpa [innerAt] using h1015 have hleft :1016 innerAt (S (n + 1)).left1017 ((innerAt (S n).right).symm (transportDense j)) =1018 outputAutomorphisms rho hrho sigma hsigma xi eta hxi heta n1019 (transportDense j) := by1020 rw [outputAutomorphisms_eq]1021 rfl1022 rw [hleft, (innerAt (S n).right).apply_symm_apply] at h'1023 exact h'10241025theorem tendsto_outputAutomorphisms_state :1026 ∀ a, Tendsto (fun n => Representation.vectorFunctional rho xi1027 (outputAutomorphisms rho hrho sigma hsigma xi eta hxi heta n a))1028 atTop (nhds (Representation.vectorFunctional sigma eta a)) := by1029 apply MathlibAnnex.CStarAlgebra.tendsto_functional_of_dense_prefix1030 transportDense denseRange_transportDense1031 (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_zero1037 exact outputAutomorphisms_state_dense rho hrho sigma hsigma xi eta hxi heta10381039/-- 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.trans1042 (leftLimitAutomorphism rho hrho sigma hsigma xi eta hxi heta)10431044/-- 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 t10481049noncomputable def implementingAutomorphism (t : ℝ) : StarAlgEquiv ℂ Limit Limit :=1050 Unitary.conjStarAlgAut ℂ Limit1051 (implementingUnitary rho hrho sigma hsigma xi eta hxi heta t)10521053theorem continuous_implementingUnitary :1054 Continuous (implementingUnitary rho hrho sigma hsigma xi eta hxi heta) := by1055 unfold implementingUnitary1056 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_leftContinuousPath1060 rho hrho sigma hsigma xi eta hxi heta).inv.mul1061 (continuous_rightContinuousPath rho hrho sigma hsigma xi eta hxi heta)10621063theorem implementingUnitary_zero :1064 implementingUnitary rho hrho sigma hsigma xi eta hxi heta 0 = 1 := by1065 simp [implementingUnitary,1066 leftContinuousPath_zero rho hrho sigma hsigma xi eta hxi heta,1067 rightContinuousPath_zero rho hrho sigma hsigma xi eta hxi heta]10681069theorem 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.trans1072 (innerAt (leftContinuousPath rho hrho sigma hsigma xi eta hxi heta t)) := by1073 ext a1074 simp [implementingAutomorphism, implementingUnitary, innerAt, mul_assoc]10751076theorem 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.trans1079 (innerAt (rightContinuousPath rho hrho sigma hsigma xi eta hxi heta t)) := by1080 rw [implementingAutomorphism_eq]1081 rfl10821083theorem tendsto_outputAutomorphisms_asymptoticAutomorphism (a : Limit) :1084 Tendsto (fun n => outputAutomorphisms1085 rho hrho sigma hsigma xi eta hxi heta n a)1086 atTop (nhds (asymptoticAutomorphism1087 rho hrho sigma hsigma xi eta hxi heta a)) := by1088 have hright : Tendsto (fun n =>1089 (rightAutomorphisms rho hrho sigma hsigma xi eta hxi heta n).symm a)1090 atTop (nhds ((rightLimitAutomorphism1091 rho hrho sigma hsigma xi eta hxi heta).symm a)) := by1092 rw [rightLimitAutomorphism,1093 MathlibAnnex.CStarAlgebra.twoSidedPointwiseLimit_symm_apply]1094 exact MathlibAnnex.CStarAlgebra.tendsto_pointwiseLimit1095 (fun n => (rightAutomorphisms1096 rho hrho sigma hsigma xi eta hxi heta n).symm)1097 (rightAutomorphisms_symm_cauchy1098 rho hrho sigma hsigma xi eta hxi heta) a1099 have hleft (b : Limit) : Tendsto (fun n =>1100 leftAutomorphisms rho hrho sigma hsigma xi eta hxi heta (n + 1) b)1101 atTop (nhds (leftLimitAutomorphism1102 rho hrho sigma hsigma xi eta hxi heta b)) := by1103 apply (tendsto_add_atTop_iff_nat1104 (f := fun n => leftAutomorphisms1105 rho hrho sigma hsigma xi eta hxi heta n b) 1).21106 simpa [leftLimitAutomorphism,1107 MathlibAnnex.CStarAlgebra.twoSidedPointwiseLimit_apply,1108 MathlibAnnex.CStarAlgebra.pointwiseLimitHom_apply] using1109 MathlibAnnex.CStarAlgebra.tendsto_pointwiseLimit1110 (leftAutomorphisms rho hrho sigma hsigma xi eta hxi heta)1111 (leftAutomorphisms_cauchy1112 rho hrho sigma hsigma xi eta hxi heta) b1113 have hcomp := MathlibAnnex.Metric.tendsto_comp_of_isometry1114 (fun n => leftAutomorphisms1115 rho hrho sigma hsigma xi eta hxi heta (n + 1))1116 (fun n => (rightAutomorphisms1117 rho hrho sigma hsigma xi eta hxi heta n).symm a)1118 (fun n => StarAlgEquiv.isometry1119 (leftAutomorphisms rho hrho sigma hsigma xi eta hxi heta (n + 1)))1120 hright (hleft ((rightLimitAutomorphism1121 rho hrho sigma hsigma xi eta hxi heta).symm a))1122 simpa [outputAutomorphisms_eq, asymptoticAutomorphism] using hcomp11231124theorem tendsto_implementingAutomorphism (a : Limit) :1125 Tendsto (fun t : ℝ =>1126 implementingAutomorphism rho hrho sigma hsigma xi eta hxi heta t a)1127 atTop (nhds (asymptoticAutomorphism1128 rho hrho sigma hsigma xi eta hxi heta a)) := by1129 have hcomp := MathlibAnnex.Metric.tendsto_comp_of_isometry1130 (fun t => innerAt1131 (leftContinuousPath rho hrho sigma hsigma xi eta hxi heta t))1132 (fun t => (innerAt1133 (rightContinuousPath rho hrho sigma hsigma xi eta hxi heta t)).symm a)1134 (fun t => StarAlgEquiv.isometry1135 (innerAt (leftContinuousPath rho hrho sigma hsigma xi eta hxi heta t)))1136 (tendsto_rightContinuousPath_inverse1137 rho hrho sigma hsigma xi eta hxi heta a)1138 (tendsto_leftContinuousPath_forward rho hrho sigma hsigma xi eta hxi heta1139 ((rightLimitAutomorphism rho hrho sigma hsigma xi eta hxi heta).symm a))1140 simpa [implementingAutomorphism_eq, asymptoticAutomorphism] using hcomp11411142theorem 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 ((asymptoticAutomorphism1146 rho hrho sigma hsigma xi eta hxi heta).symm a)) := by1147 have hcomp := MathlibAnnex.Metric.tendsto_comp_of_isometry1148 (fun t => innerAt1149 (rightContinuousPath rho hrho sigma hsigma xi eta hxi heta t))1150 (fun t => (innerAt1151 (leftContinuousPath rho hrho sigma hsigma xi eta hxi heta t)).symm a)1152 (fun t => StarAlgEquiv.isometry1153 (innerAt (rightContinuousPath rho hrho sigma hsigma xi eta hxi heta t)))1154 (tendsto_leftContinuousPath_inverse1155 rho hrho sigma hsigma xi eta hxi heta a)1156 (tendsto_rightContinuousPath_forward rho hrho sigma hsigma xi eta hxi heta1157 ((leftLimitAutomorphism rho hrho sigma hsigma xi eta hxi heta).symm a))1158 simpa [implementingAutomorphism_symm_eq, asymptoticAutomorphism] using hcomp11591160theorem asymptoticAutomorphism_state (a : Limit) :1161 Representation.vectorFunctional rho xi1162 (asymptoticAutomorphism rho hrho sigma hsigma xi eta hxi heta a) =1163 Representation.vectorFunctional sigma eta a := by1164 apply tendsto_nhds_unique1165 ((Representation.vectorFunctional rho xi).continuous.tendsto _ |>.comp1166 (tendsto_outputAutomorphisms_asymptoticAutomorphism1167 rho hrho sigma hsigma xi eta hxi heta a))1168 exact tendsto_outputAutomorphisms_state1169 rho hrho sigma hsigma xi eta hxi heta a11701171include hrho hsigma hxi heta in1172theorem 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)) := by1182 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⟩11891190include hrho hsigma hxi heta in1191theorem hasInnerIntertwiningSequence_vectorFunctional :1192 HasInnerIntertwiningSequence1193 (Representation.vectorFunctional rho xi)1194 (Representation.vectorFunctional sigma eta) := by1195 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 n1200 exact ⟨outputUnitary rho hrho sigma hsigma xi eta hxi heta n, rfl⟩12011202end Sequences12031204set_option maxHeartbeats 1600000 in1205/-- Every pair of pure CAR states has a genuine two-sided inner1206intertwining sequence. -/1207theorem hasInnerIntertwiningSequence_of_pure1208 (phi psi : Limit →L[ℂ] ℂ)1209 (hphi : MathlibAnnex.CStarAlgebra.IsPureState Limit phi) (hpsi : MathlibAnnex.CStarAlgebra.IsPureState Limit psi) :1210 HasInnerIntertwiningSequence phi psi := by1211 have hphiState : phi ∈ stateSpace Limit := extremePoints_subset hphi1212 let fphi := positiveLinearMapOfMemStateSpace phi hphiState1213 let rho : Representation Limit fphi.GNS := fphi.gnsStarAlgHom1214 let xi : fphi.GNS := fphi.gnsCyclicVector1215 have hxi : ‖xi‖ = 1 := by1216 change ‖stateGNSVector phi hphiState‖ = 11217 exact norm_stateGNSVector phi hphiState1218 letI : Nontrivial fphi.GNS := by1219 apply nontrivial_of_ne xi 01220 intro hzero1221 have hnorm := congrArg norm hzero1222 rw [hxi, norm_zero] at hnorm1223 norm_num at hnorm1224 have hrho : StarAlgHom.IsIrreducible rho := by1225 simpa [rho, fphi] using1226 isIrreducible_pureState_gnsStarAlgHom phi hphiState hphi1227 have hphiVF : Representation.vectorFunctional rho xi = phi := by1228 apply ContinuousLinearMap.ext1229 intro a1230 rw [Representation.vectorFunctional_apply]1231 change inner ℂ (stateGNSVector phi hphiState)1232 ((positiveLinearMapOfMemStateSpace phi hphiState).gnsStarAlgHom a1233 (stateGNSVector phi hphiState)) = phi a1234 exact inner_gnsStarAlgHom_stateGNSVector phi hphiState a1235 have hpsiState : psi ∈ stateSpace Limit := extremePoints_subset hpsi1236 let fpsi := positiveLinearMapOfMemStateSpace psi hpsiState1237 let sigma : Representation Limit fpsi.GNS := fpsi.gnsStarAlgHom1238 let eta : fpsi.GNS := fpsi.gnsCyclicVector1239 have heta : ‖eta‖ = 1 := by1240 change ‖stateGNSVector psi hpsiState‖ = 11241 exact norm_stateGNSVector psi hpsiState1242 letI : Nontrivial fpsi.GNS := by1243 apply nontrivial_of_ne eta 01244 intro hzero1245 have hnorm := congrArg norm hzero1246 rw [heta, norm_zero] at hnorm1247 norm_num at hnorm1248 have hsigma : StarAlgHom.IsIrreducible sigma := by1249 simpa [sigma, fpsi] using1250 isIrreducible_pureState_gnsStarAlgHom psi hpsiState hpsi1251 have hpsiVF : Representation.vectorFunctional sigma eta = psi := by1252 apply ContinuousLinearMap.ext1253 intro a1254 rw [Representation.vectorFunctional_apply]1255 change inner ℂ (stateGNSVector psi hpsiState)1256 ((positiveLinearMapOfMemStateSpace psi hpsiState).gnsStarAlgHom a1257 (stateGNSVector psi hpsiState)) = psi a1258 exact inner_gnsStarAlgHom_stateGNSVector psi hpsiState a1259 rw [← hphiVF, ← hpsiVF]1260 exact hasInnerIntertwiningSequence_vectorFunctional1261 rho hrho sigma hsigma xi eta hxi heta12621263set_option maxHeartbeats 1600000 in1264/-- Every pair of pure CAR states is connected by one norm-continuous1265unitary path whose inner automorphisms, and their actual inverses, converge1266point-norm to the transporting automorphism and its inverse. -/1267theorem asymptoticallyInnerPureStateHomogeneity : AsymptoticallyInnerPureStateHomogeneity := by1268 intro phi psi hphi hpsi1269 have hphiState : phi ∈ stateSpace Limit := extremePoints_subset hphi1270 let fphi := positiveLinearMapOfMemStateSpace phi hphiState1271 let rho : Representation Limit fphi.GNS := fphi.gnsStarAlgHom1272 let xi : fphi.GNS := fphi.gnsCyclicVector1273 have hxi : ‖xi‖ = 1 := by1274 change ‖stateGNSVector phi hphiState‖ = 11275 exact norm_stateGNSVector phi hphiState1276 letI : Nontrivial fphi.GNS := by1277 apply nontrivial_of_ne xi 01278 intro hzero1279 have hnorm := congrArg norm hzero1280 rw [hxi, norm_zero] at hnorm1281 norm_num at hnorm1282 have hrho : StarAlgHom.IsIrreducible rho := by1283 simpa [rho, fphi] using1284 isIrreducible_pureState_gnsStarAlgHom phi hphiState hphi1285 have hphiVF : Representation.vectorFunctional rho xi = phi := by1286 apply ContinuousLinearMap.ext1287 intro a1288 rw [Representation.vectorFunctional_apply]1289 change inner ℂ (stateGNSVector phi hphiState)1290 ((positiveLinearMapOfMemStateSpace phi hphiState).gnsStarAlgHom a1291 (stateGNSVector phi hphiState)) = phi a1292 exact inner_gnsStarAlgHom_stateGNSVector phi hphiState a1293 have hpsiState : psi ∈ stateSpace Limit := extremePoints_subset hpsi1294 let fpsi := positiveLinearMapOfMemStateSpace psi hpsiState1295 let sigma : Representation Limit fpsi.GNS := fpsi.gnsStarAlgHom1296 let eta : fpsi.GNS := fpsi.gnsCyclicVector1297 have heta : ‖eta‖ = 1 := by1298 change ‖stateGNSVector psi hpsiState‖ = 11299 exact norm_stateGNSVector psi hpsiState1300 letI : Nontrivial fpsi.GNS := by1301 apply nontrivial_of_ne eta 01302 intro hzero1303 have hnorm := congrArg norm hzero1304 rw [heta, norm_zero] at hnorm1305 norm_num at hnorm1306 have hsigma : StarAlgHom.IsIrreducible sigma := by1307 simpa [sigma, fpsi] using1308 isIrreducible_pureState_gnsStarAlgHom psi hpsiState hpsi1309 have hpsiVF : Representation.vectorFunctional sigma eta = psi := by1310 apply ContinuousLinearMap.ext1311 intro a1312 rw [Representation.vectorFunctional_apply]1313 change inner ℂ (stateGNSVector psi hpsiState)1314 ((positiveLinearMapOfMemStateSpace psi hpsiState).gnsStarAlgHom a1315 (stateGNSVector psi hpsiState)) = psi a1316 exact inner_gnsStarAlgHom_stateGNSVector psi hpsiState a1317 obtain ⟨alpha, U, hU, hU0, hstate, hforward, hinverse⟩ :=1318 asymptoticallyInner_vectorFunctional1319 rho hrho sigma hsigma xi eta hxi heta1320 refine ⟨alpha, U, hU, hU0, ?_, hforward, hinverse⟩1321 intro a1322 rw [← hphiVF, ← hpsiVF]1323 exact hstate a13241325/-- Regression adapter: forgetting the implementing path recovers the1326previous CAR approximate-inner homogeneity statement. -/1327theorem homogeneity_from_asymptotic : PureStateHomogeneity :=1328 homogeneity_of_asymptoticallyInner asymptoticallyInnerPureStateHomogeneity13291330/-- The CAR homogeneity endpoint, with the intertwining supplier discharged. -/1331theorem homogeneity : PureStateHomogeneity :=1332 homogeneity_of_innerIntertwiningSequences1333 (fun phi psi hphi hpsi =>1334 hasInnerIntertwiningSequence_of_pure phi psi hphi hpsi)13351336end MathlibAnnex.CStarAlgebra.CAR