Exact source: MathlibAnnex/Analysis/CStarAlgebra/CAR/StateTransport.lean
Pinned GitHub source · Raw UTF-8 source
Back to Cross-representation state approximation with a protected finite set · Back to Pure CAR states admit two-sided inner intertwining sequences
1import MathlibAnnex.Analysis.CStarAlgebra.CAR.LocalTransport2import MathlibAnnex.Analysis.CStarAlgebra.CAR.StagePurification34/-!5# Local transport of CAR vector states67This file separates the exact same-representation correction from the8finite-stage approximation used between different representations. The9protected finite set and its tolerance are fixed before the state tests; a10later target finite set is handled by finite-stage purification.11-/1213set_option autoImplicit false1415noncomputable section1617open MathlibAnnex.Analysis.CStarAlgebra1819namespace MathlibAnnex.CStarAlgebra.CAR2021set_option maxHeartbeats 800000 in22/-- A target vector state in another representation can be approximated on23any later finite set while the implementing inner automorphism nearly fixes24an earlier protected finite set. Closeness on the fixed stage tests is the25only hypothesis connecting the two original vector states. -/26theorem exists_stageTests_crossRepresentation_path_approx27 {H : Type*}28 [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]29 [Nontrivial H]30 (rho : Representation Limit H) (hrho : StarAlgHom.IsIrreducible rho)31 (F : Finset Limit) {epsilon : ℝ} (hepsilon : 0 < epsilon) :32 ∃ n, ∃ delta > 0,33 ∀ {K : Type*}34 [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K]35 (sigma : Representation Limit K) (xi : H) (eta : K),36 ‖xi‖ = 1 → ‖eta‖ = 1 →37 (∀ i j : Fin (2 ^ n),38 ‖Representation.vectorFunctional rho xi (limitMatrixUnit n i j) -39 Representation.vectorFunctional sigma eta (limitMatrixUnit n i j)‖ < delta) →40 ∀ (F' : Finset Limit) (epsilon' : ℝ), 0 < epsilon' →41 ∃ u : unitary Limit,42 ∃ p : Path 1 u,43 (∀ t, ∀ a ∈ F,44 ‖(p t : Limit) * a * star (p t : Limit) - a‖ < epsilon ∧45 ‖star (p t : Limit) * a * (p t : Limit) - a‖ < epsilon) ∧46 ∀ a ∈ F',47 ‖Representation.vectorFunctional rho (rho (u : Limit) xi) a -48 Representation.vectorFunctional sigma eta a‖ < epsilon' := by49 classical50 obtain ⟨n, delta, hdelta, hlocal⟩ :=51 exists_stageTests_exact_unitary_path_apply_eq_and_conjugate_sub_norm_lt52 rho hrho F hepsilon53 refine ⟨n, delta, hdelta, ?_⟩54 intro K _ _ _ sigma xi eta hxi heta hstate F' epsilon' hepsilon'55 obtain ⟨m, hm⟩ := exists_common_stage_approx F'56 (show 0 < epsilon' / 3 by positivity)57 let N : ℕ := max n m58 have hnN : n ≤ N := le_max_left n m59 have hmN : m ≤ N := le_max_right n m60 obtain ⟨zeta, hzeta, hzstage⟩ :=61 exists_unitVector_vectorFunctional_eq_on_stage rho62 ((Representation.isIrreducible_iff_starAlgHom rho).mpr hrho)63 sigma N eta heta64 have hzmatrix (i j : Fin (2 ^ n)) :65 Representation.vectorFunctional rho zeta (limitMatrixUnit n i j) =66 Representation.vectorFunctional sigma eta (limitMatrixUnit n i j) := by67 have h := hzstage (embed n N hnN (matrixUnit n i j))68 simpa only [ofStage_embed, limitMatrixUnit] using h69 obtain ⟨u, huapply, p, huprotect⟩ := hlocal xi zeta hxi hzeta (by70 intro i j71 rw [hzmatrix i j]72 exact hstate i j)73 refine ⟨u, p, huprotect, ?_⟩74 intro a ha75 obtain ⟨c, hc⟩ := hm a ha76 let d : Limit := ofStage N (embed m N hmN c)77 have hd : d = ofStage m c := by78 dsimp only [d]79 rw [ofStage_embed]80 have htarget :81 Representation.vectorFunctional rho zeta d =82 Representation.vectorFunctional sigma eta d := by83 dsimp only [d]84 exact hzstage (embed m N hmN c)85 rw [huapply]86 have hdecomp :87 Representation.vectorFunctional rho zeta a -88 Representation.vectorFunctional sigma eta a =89 Representation.vectorFunctional rho zeta (a - d) +90 Representation.vectorFunctional sigma eta (d - a) := by91 rw [map_sub, map_sub, htarget]92 ring93 rw [hdecomp]94 calc95 _ ≤ ‖Representation.vectorFunctional rho zeta (a - d)‖ +96 ‖Representation.vectorFunctional sigma eta (d - a)‖ := norm_add_le _ _97 _ ≤ ‖a - d‖ + ‖d - a‖ := by98 exact add_le_add99 (Representation.norm_vectorFunctional_apply_le rho hzeta (a - d))100 (Representation.norm_vectorFunctional_apply_le sigma heta (d - a))101 _ = 2 * ‖a - d‖ := by rw [norm_sub_rev d a]; ring102 _ < epsilon' := by103 rw [hd]104 linarith105106set_option maxHeartbeats 800000 in107/-- Endpoint-only compatibility wrapper for108`exists_stageTests_crossRepresentation_path_approx`. -/109theorem exists_stageTests_crossRepresentation_approx110 {H : Type*}111 [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]112 [Nontrivial H]113 (rho : Representation Limit H) (hrho : StarAlgHom.IsIrreducible rho)114 (F : Finset Limit) {epsilon : ℝ} (hepsilon : 0 < epsilon) :115 ∃ n, ∃ delta > 0,116 ∀ {K : Type*}117 [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K]118 (sigma : Representation Limit K) (xi : H) (eta : K),119 ‖xi‖ = 1 → ‖eta‖ = 1 →120 (∀ i j : Fin (2 ^ n),121 ‖Representation.vectorFunctional rho xi (limitMatrixUnit n i j) -122 Representation.vectorFunctional sigma eta (limitMatrixUnit n i j)‖ < delta) →123 ∀ (F' : Finset Limit) (epsilon' : ℝ), 0 < epsilon' →124 ∃ u : unitary Limit,125 (∀ a ∈ F,126 ‖(u : Limit) * a * star (u : Limit) - a‖ < epsilon ∧127 ‖star (u : Limit) * a * (u : Limit) - a‖ < epsilon) ∧128 ∀ a ∈ F',129 ‖Representation.vectorFunctional rho (rho (u : Limit) xi) a -130 Representation.vectorFunctional sigma eta a‖ < epsilon' := by131 obtain ⟨n, delta, hdelta, hmain⟩ :=132 exists_stageTests_crossRepresentation_path_approx rho hrho F hepsilon133 refine ⟨n, delta, hdelta, ?_⟩134 intro K _ _ _ sigma xi eta hxi heta hstate F' epsilon' hepsilon'135 obtain ⟨u, p, hprotect, happrox⟩ :=136 hmain sigma xi eta hxi heta hstate F' epsilon' hepsilon'137 refine ⟨u, ?_, happrox⟩138 intro a ha139 simpa only [p.target] using hprotect (1 : Set.Icc (0 : ℝ) 1) a ha140141set_option maxHeartbeats 800000 in142/-- With no near-centrality requirement, one irreducible CAR representation143can approximate an arbitrary unit vector state from another representation on144any finite set. Stage zero supplies the exact transitivity step, while145finite-stage purification supplies the requested state accuracy. -/146theorem exists_unitary_crossRepresentation_path_approx147 {H K : Type*}148 [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]149 [Nontrivial H]150 [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K]151 (rho : Representation Limit H) (hrho : StarAlgHom.IsIrreducible rho)152 (sigma : Representation Limit K) (xi : H) (eta : K)153 (hxi : ‖xi‖ = 1) (heta : ‖eta‖ = 1)154 (F : Finset Limit) {epsilon : ℝ} (hepsilon : 0 < epsilon) :155 ∃ u : unitary Limit, ∃ p : Path 1 u, ∀ a ∈ F,156 ‖Representation.vectorFunctional rho (rho (u : Limit) xi) a -157 Representation.vectorFunctional sigma eta a‖ < epsilon := by158 classical159 obtain ⟨m, hm⟩ := exists_common_stage_approx F160 (show 0 < epsilon / 3 by positivity)161 obtain ⟨zeta, hzeta, hzstage⟩ :=162 exists_unitVector_vectorFunctional_eq_on_stage rho163 ((Representation.isIrreducible_iff_starAlgHom rho).mpr hrho)164 sigma m eta heta165 obtain ⟨delta, hdelta, htrans⟩ :=166 exists_delta_exact_unitary_path_apply_eq_and_stage_commutator167 rho hrho 0 (by norm_num : (0 : ℝ) < 1)168 obtain ⟨u, huapply, p, _⟩ := htrans xi zeta hxi hzeta (by169 intro i j170 have hunit : limitMatrixUnit 0 (0 : Fin (2 ^ 0)) (0 : Fin (2 ^ 0)) = 1 := by171 simpa using sum_limitMatrixUnit_diag 0172 have hij : limitMatrixUnit 0 i j = 1 := by173 rw [← hunit]174 congr <;> apply Fin.ext <;> simp175 rw [hij, Representation.vectorFunctional_one rho hxi,176 Representation.vectorFunctional_one rho hzeta, sub_self, norm_zero]177 exact hdelta)178 refine ⟨u, p, ?_⟩179 intro a ha180 obtain ⟨c, hc⟩ := hm a ha181 have htarget := hzstage c182 rw [huapply]183 have hdecomp :184 Representation.vectorFunctional rho zeta a -185 Representation.vectorFunctional sigma eta a =186 Representation.vectorFunctional rho zeta (a - ofStage m c) +187 Representation.vectorFunctional sigma eta (ofStage m c - a) := by188 rw [map_sub, map_sub, htarget]189 ring190 rw [hdecomp]191 calc192 _ ≤ ‖Representation.vectorFunctional rho zeta (a - ofStage m c)‖ +193 ‖Representation.vectorFunctional sigma eta (ofStage m c - a)‖ :=194 norm_add_le _ _195 _ ≤ ‖a - ofStage m c‖ + ‖ofStage m c - a‖ := by196 exact add_le_add197 (Representation.norm_vectorFunctional_apply_le rho hzeta _)198 (Representation.norm_vectorFunctional_apply_le sigma heta _)199 _ = 2 * ‖a - ofStage m c‖ := by200 rw [norm_sub_rev (ofStage m c) a]201 ring202 _ < epsilon := by linarith203204set_option maxHeartbeats 800000 in205/-- Endpoint-only compatibility wrapper for206`exists_unitary_crossRepresentation_path_approx`. -/207theorem exists_unitary_crossRepresentation_approx208 {H K : Type*}209 [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]210 [Nontrivial H]211 [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K]212 (rho : Representation Limit H) (hrho : StarAlgHom.IsIrreducible rho)213 (sigma : Representation Limit K) (xi : H) (eta : K)214 (hxi : ‖xi‖ = 1) (heta : ‖eta‖ = 1)215 (F : Finset Limit) {epsilon : ℝ} (hepsilon : 0 < epsilon) :216 ∃ u : unitary Limit, ∀ a ∈ F,217 ‖Representation.vectorFunctional rho (rho (u : Limit) xi) a -218 Representation.vectorFunctional sigma eta a‖ < epsilon := by219 obtain ⟨u, -, happrox⟩ := exists_unitary_crossRepresentation_path_approx220 rho hrho sigma xi eta hxi heta F hepsilon221 exact ⟨u, happrox⟩222223set_option maxHeartbeats 800000 in224/-- Pure-state form of cross-representation local transport. For a fixed225source pure state and protected finite set, the finite stage tests are chosen226before the target pure state and before the later approximation request. -/227theorem exists_stageTests_pureState_path_approx228 (phi : Limit →L[ℂ] ℂ) (hphi : MathlibAnnex.CStarAlgebra.IsPureState Limit phi)229 (F : Finset Limit) {epsilon : ℝ} (hepsilon : 0 < epsilon) :230 ∃ n, ∃ delta > 0,231 ∀ (psi : Limit →L[ℂ] ℂ), MathlibAnnex.CStarAlgebra.IsPureState Limit psi →232 (∀ i j : Fin (2 ^ n),233 ‖phi (limitMatrixUnit n i j) - psi (limitMatrixUnit n i j)‖ < delta) →234 ∀ (F' : Finset Limit) (epsilon' : ℝ), 0 < epsilon' →235 ∃ u : unitary Limit,236 ∃ p : Path 1 u,237 (∀ t, ∀ a ∈ F,238 ‖star (p t : Limit) * a * (p t : Limit) - a‖ < epsilon) ∧239 ∀ a ∈ F',240 ‖phi (star (u : Limit) * a * (u : Limit)) - psi a‖ < epsilon' := by241 have hphiState : phi ∈ stateSpace Limit := extremePoints_subset hphi242 let fphi := positiveLinearMapOfMemStateSpace phi hphiState243 let rho : Representation Limit fphi.GNS := fphi.gnsStarAlgHom244 let xi : fphi.GNS := fphi.gnsCyclicVector245 have hxi : ‖xi‖ = 1 := by246 change ‖stateGNSVector phi hphiState‖ = 1247 exact norm_stateGNSVector phi hphiState248 letI : Nontrivial fphi.GNS := by249 apply nontrivial_of_ne xi 0250 intro hzero251 have hnorm := congrArg norm hzero252 rw [hxi, norm_zero] at hnorm253 norm_num at hnorm254 have hrho : StarAlgHom.IsIrreducible rho := by255 simpa [rho, fphi] using256 isIrreducible_pureState_gnsStarAlgHom phi hphiState hphi257 have hphiVF : Representation.vectorFunctional rho xi = phi := by258 apply ContinuousLinearMap.ext259 intro a260 rw [Representation.vectorFunctional_apply]261 change inner ℂ (stateGNSVector phi hphiState)262 ((positiveLinearMapOfMemStateSpace phi hphiState).gnsStarAlgHom a263 (stateGNSVector phi hphiState)) = phi a264 exact inner_gnsStarAlgHom_stateGNSVector phi hphiState a265 obtain ⟨n, delta, hdelta, hcross⟩ :=266 exists_stageTests_crossRepresentation_path_approx rho hrho F hepsilon267 refine ⟨n, delta, hdelta, ?_⟩268 intro psi hpsi hstate F' epsilon' hepsilon'269 have hpsiState : psi ∈ stateSpace Limit := extremePoints_subset hpsi270 let fpsi := positiveLinearMapOfMemStateSpace psi hpsiState271 let sigma : Representation Limit fpsi.GNS := fpsi.gnsStarAlgHom272 let eta : fpsi.GNS := fpsi.gnsCyclicVector273 have heta : ‖eta‖ = 1 := by274 change ‖stateGNSVector psi hpsiState‖ = 1275 exact norm_stateGNSVector psi hpsiState276 have hpsiVF : Representation.vectorFunctional sigma eta = psi := by277 apply ContinuousLinearMap.ext278 intro a279 rw [Representation.vectorFunctional_apply]280 change inner ℂ (stateGNSVector psi hpsiState)281 ((positiveLinearMapOfMemStateSpace psi hpsiState).gnsStarAlgHom a282 (stateGNSVector psi hpsiState)) = psi a283 exact inner_gnsStarAlgHom_stateGNSVector psi hpsiState a284 obtain ⟨u, p, hprotect, happrox⟩ :=285 hcross sigma xi eta hxi heta (by286 intro i j287 rw [hphiVF, hpsiVF]288 exact hstate i j) F' epsilon' hepsilon'289 refine ⟨u, p, (fun t a ha => (hprotect t a ha).2), ?_⟩290 intro a ha291 have h := happrox a ha292 rw [Representation.vectorFunctional_map_apply, hphiVF, hpsiVF] at h293 exact h294295set_option maxHeartbeats 800000 in296/-- Endpoint-only compatibility wrapper for297`exists_stageTests_pureState_path_approx`. -/298theorem exists_stageTests_pureState_approx299 (phi : Limit →L[ℂ] ℂ) (hphi : MathlibAnnex.CStarAlgebra.IsPureState Limit phi)300 (F : Finset Limit) {epsilon : ℝ} (hepsilon : 0 < epsilon) :301 ∃ n, ∃ delta > 0,302 ∀ (psi : Limit →L[ℂ] ℂ), MathlibAnnex.CStarAlgebra.IsPureState Limit psi →303 (∀ i j : Fin (2 ^ n),304 ‖phi (limitMatrixUnit n i j) - psi (limitMatrixUnit n i j)‖ < delta) →305 ∀ (F' : Finset Limit) (epsilon' : ℝ), 0 < epsilon' →306 ∃ u : unitary Limit,307 (∀ a ∈ F,308 ‖star (u : Limit) * a * (u : Limit) - a‖ < epsilon) ∧309 ∀ a ∈ F',310 ‖phi (star (u : Limit) * a * (u : Limit)) - psi a‖ < epsilon' := by311 obtain ⟨n, delta, hdelta, hmain⟩ :=312 exists_stageTests_pureState_path_approx phi hphi F hepsilon313 refine ⟨n, delta, hdelta, ?_⟩314 intro psi hpsi hstate F' epsilon' hepsilon'315 obtain ⟨u, p, hprotect, happrox⟩ :=316 hmain psi hpsi hstate F' epsilon' hepsilon'317 refine ⟨u, ?_, happrox⟩318 intro a ha319 simpa only [p.target] using hprotect (1 : Set.Icc (0 : ℝ) 1) a ha320321set_option maxHeartbeats 800000 in322/-- Any pure CAR state can be approximated on a finite set by an inner323translate of any other pure state. This is the unprotected initialization324step for the alternating intertwining construction. -/325theorem exists_unitary_pureState_path_approx326 (phi psi : Limit →L[ℂ] ℂ)327 (hphi : MathlibAnnex.CStarAlgebra.IsPureState Limit phi) (hpsi : MathlibAnnex.CStarAlgebra.IsPureState Limit psi)328 (F : Finset Limit) {epsilon : ℝ} (hepsilon : 0 < epsilon) :329 ∃ u : unitary Limit, ∃ p : Path 1 u, ∀ a ∈ F,330 ‖phi (star (u : Limit) * a * (u : Limit)) - psi a‖ < epsilon := by331 have hphiState : phi ∈ stateSpace Limit := extremePoints_subset hphi332 let fphi := positiveLinearMapOfMemStateSpace phi hphiState333 let rho : Representation Limit fphi.GNS := fphi.gnsStarAlgHom334 let xi : fphi.GNS := fphi.gnsCyclicVector335 have hxi : ‖xi‖ = 1 := by336 change ‖stateGNSVector phi hphiState‖ = 1337 exact norm_stateGNSVector phi hphiState338 letI : Nontrivial fphi.GNS := by339 apply nontrivial_of_ne xi 0340 intro hzero341 have hnorm := congrArg norm hzero342 rw [hxi, norm_zero] at hnorm343 norm_num at hnorm344 have hrho : StarAlgHom.IsIrreducible rho := by345 simpa [rho, fphi] using346 isIrreducible_pureState_gnsStarAlgHom phi hphiState hphi347 have hphiVF : Representation.vectorFunctional rho xi = phi := by348 apply ContinuousLinearMap.ext349 intro a350 rw [Representation.vectorFunctional_apply]351 change inner ℂ (stateGNSVector phi hphiState)352 ((positiveLinearMapOfMemStateSpace phi hphiState).gnsStarAlgHom a353 (stateGNSVector phi hphiState)) = phi a354 exact inner_gnsStarAlgHom_stateGNSVector phi hphiState a355 have hpsiState : psi ∈ stateSpace Limit := extremePoints_subset hpsi356 let fpsi := positiveLinearMapOfMemStateSpace psi hpsiState357 let sigma : Representation Limit fpsi.GNS := fpsi.gnsStarAlgHom358 let eta : fpsi.GNS := fpsi.gnsCyclicVector359 have heta : ‖eta‖ = 1 := by360 change ‖stateGNSVector psi hpsiState‖ = 1361 exact norm_stateGNSVector psi hpsiState362 have hpsiVF : Representation.vectorFunctional sigma eta = psi := by363 apply ContinuousLinearMap.ext364 intro a365 rw [Representation.vectorFunctional_apply]366 change inner ℂ (stateGNSVector psi hpsiState)367 ((positiveLinearMapOfMemStateSpace psi hpsiState).gnsStarAlgHom a368 (stateGNSVector psi hpsiState)) = psi a369 exact inner_gnsStarAlgHom_stateGNSVector psi hpsiState a370 obtain ⟨u, p, hu⟩ := exists_unitary_crossRepresentation_path_approx371 rho hrho sigma xi eta hxi heta F hepsilon372 refine ⟨u, p, ?_⟩373 intro a ha374 have h := hu a ha375 rw [Representation.vectorFunctional_map_apply, hphiVF, hpsiVF] at h376 exact h377378set_option maxHeartbeats 800000 in379/-- Endpoint-only compatibility wrapper for380`exists_unitary_pureState_path_approx`. -/381theorem exists_unitary_pureState_approx382 (phi psi : Limit →L[ℂ] ℂ)383 (hphi : MathlibAnnex.CStarAlgebra.IsPureState Limit phi) (hpsi : MathlibAnnex.CStarAlgebra.IsPureState Limit psi)384 (F : Finset Limit) {epsilon : ℝ} (hepsilon : 0 < epsilon) :385 ∃ u : unitary Limit, ∀ a ∈ F,386 ‖phi (star (u : Limit) * a * (u : Limit)) - psi a‖ < epsilon := by387 obtain ⟨u, -, happrox⟩ :=388 exists_unitary_pureState_path_approx phi psi hphi hpsi F hepsilon389 exact ⟨u, happrox⟩390391end MathlibAnnex.CStarAlgebra.CAR