Exact source: MathlibAnnex/Analysis/CStarAlgebra/CAR/LocalTransport.lean, lines 353–455.
Back to Exact vector transport along an almost central unitary path · Back to Approximating another vector state along a unitary path
1import MathlibAnnex.Analysis.CStarAlgebra.CAR.InvolutionLift 2import MathlibAnnex.Analysis.InnerProductSpace.GramPerturbation 3import MathlibAnnex.Analysis.InnerProductSpace.FiniteEmbedding 4 5set_option autoImplicit false 6 7noncomputable section 8 9open MathlibAnnex.Analysis.CStarAlgebra 10open MathlibAnnex.Analysis.InnerProductSpace 11open MathlibAnnex.InnerProductSpace 12 13namespace MathlibAnnex.CStarAlgebra.CAR 14 15set_option maxHeartbeats 1000000 in 16theorem exists_delta_liftedCornerUnitary_path_apply_sub_norm_lt 17 {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] 18 [CompleteSpace H] [Nontrivial H] 19 (rho : Representation Limit H) (hrho : StarAlgHom.IsIrreducible rho) 20 (n d : ℕ) {tau : ℝ} (htau : 0 < tau) : 21 ∃ delta > 0, 22 ∀ (v w : Fin d → rootCornerSubspace rho n), 23 (∑ i, ‖v i‖ ^ 2) ≤ 1 → (∑ i, ‖w i‖ ^ 2) ≤ 1 → 24 (∀ i j, ‖inner ℂ (v i) (v j) - inner ℂ (w i) (w j)‖ < delta) → 25 ∃ u : unitary Limit, 26 (∀ c : Stage n, Commute (ofStage n c) (u : Limit)) ∧ 27 (∃ p : Path 1 u, ∀ t c, 28 Commute (ofStage n c) (p t : Limit)) ∧ 29 ∀ i, ‖rho (u : Limit) (v i : H) - (w i : H)‖ < tau := by 30 obtain ⟨delta, hdelta, hperturb⟩ := 31 exists_delta_orthogonalGramPerturbation (n := d) (half_pos htau) 32 refine ⟨delta, hdelta, ?_⟩ 33 intro v w hv hw hgram 34 let e : Limit := limitMatrixUnit n 0 0 35 let K : Submodule ℂ H := rootCornerSubspace rho n 36 have hroot : IsStarProjection (rho e) := 37 (isStarProjection_limitMatrixUnit_zero_zero n).map rho 38 letI : CompleteSpace K := IsComplete.completeSpace_coe 39 (ContinuousLinearMap.IsIdempotentElem.isClosed_range 40 hroot.isIdempotentElem).isComplete 41 have hKnot : ¬ FiniteDimensional ℂ K := by 42 simpa [K, e, rootCornerSubspace] using 43 not_finiteDimensional_range_rootCorner rho 44 ((Representation.isIrreducible_iff_starAlgHom rho).mpr hrho) n 45 let V : Submodule ℂ K := 46 Submodule.span ℂ (Set.range v ∪ Set.range w) 47 letI : FiniteDimensional ℂ V := 48 FiniteDimensional.span_of_finite ℂ 49 ((Set.finite_range v).union (Set.finite_range w)) 50 letI : V.HasOrthogonalProjection := inferInstance 51 let R : Submodule ℂ K := Vᗮ 52 letI : CompleteSpace R := IsComplete.completeSpace_coe 53 (show IsClosed (R : Set K) by 54 simpa [R] using Submodule.isClosed_orthogonal V).isComplete 55 have hRnot : ¬ FiniteDimensional ℂ R := by 56 intro hR 57 letI : FiniteDimensional ℂ R := hR 58 have htop : V ⊔ R = ⊤ := by 59 simpa [R] using 60 (Submodule.sup_orthogonal_of_hasOrthogonalProjection (K := V)) 61 letI : FiniteDimensional ℂ (V ⊔ R : Submodule ℂ K) := inferInstance 62 apply hKnot 63 exact FiniteDimensional.of_surjective (V ⊔ R).subtype (fun x => 64 ⟨⟨x, by rw [htop]; simp⟩, rfl⟩) 65 let S : Submodule ℂ K := Submodule.span ℂ (Set.range v) 66 letI : FiniteDimensional ℂ S := 67 FiniteDimensional.span_of_finite ℂ (Set.finite_range v) 68 obtain ⟨L⟩ := 69 nonempty_linearIsometry_of_finiteDimensional_of_not_finiteDimensional 70 (E := S) (F := R) hRnot 71 let vS : Fin d → S := fun i => 72 ⟨v i, Submodule.subset_span (Set.mem_range_self i)⟩ 73 let z : Fin d → K := fun i => (L (vS i) : R) 74 have hvV (i : Fin d) : v i ∈ V := 75 Submodule.subset_span (Or.inl (Set.mem_range_self i)) 76 have hwV (i : Fin d) : w i ∈ V := 77 Submodule.subset_span (Or.inr (Set.mem_range_self i)) 78 have hzR (i : Fin d) : z i ∈ R := (L (vS i)).property 79 have hzgram (i j : Fin d) : 80 inner ℂ (z i) (z j) = inner ℂ (v i) (v j) := by 81 change inner ℂ (L (vS i)) (L (vS j)) = inner ℂ (vS i) (vS j) 82 exact L.inner_map_map (vS i) (vS j) 83 have hzsum : (∑ i, ‖z i‖ ^ 2) ≤ 1 := by 84 calc 85 (∑ i, ‖z i‖ ^ 2) = ∑ i, ‖v i‖ ^ 2 := by 86 apply Finset.sum_congr rfl 87 intro i _ 88 rw [show ‖z i‖ = ‖v i‖ by exact L.norm_map (vS i)] 89 _ ≤ 1 := hv 90 have hvzorth : ∀ i j, inner ℂ (v i) (z j) = 0 := by 91 intro i j 92 exact V.inner_right_of_mem_orthogonal (hvV i) (hzR j) 93 have hzworth : ∀ i j, inner ℂ (z i) (w j) = 0 := by 94 intro i j 95 exact V.inner_left_of_mem_orthogonal (hwV j) (hzR i) 96 obtain ⟨U1, hU1, -, hU1sq, hU1finite⟩ := 97 hperturb v z hv hzsum hvzorth (by 98 intro i j 99 rw [hzgram] 100 simpa using hdelta) 101 obtain ⟨U2, hU2, -, hU2sq, hU2finite⟩ := 102 hperturb z w hzsum hw hzworth (by 103 intro i j 104 rw [hzgram] 105 exact hgram i j) 106 letI : FiniteDimensional ℂ 107 (LinearMap.range (U1.toLinearMap - LinearMap.id)) := hU1finite 108 obtain ⟨h1, heh1, hhe1, hu1exact⟩ := 109 exists_liftedCornerExponential_apply_eq_involution 110 rho hrho n d v U1 hU1sq 111 letI : FiniteDimensional ℂ 112 (LinearMap.range (U2.toLinearMap - LinearMap.id)) := hU2finite 113 obtain ⟨h2, heh2, hhe2, hu2exact⟩ := 114 exists_liftedCornerExponential_apply_eq_involution 115 rho hrho n d z U2 hU2sq 116 let u1 : unitary Limit := liftedCornerExponential n h1 heh1 hhe1 117 let u2 : unitary Limit := liftedCornerExponential n h2 heh2 hhe2 118 let u : unitary Limit := u2 * u1 119 refine ⟨u, ?_, ?_, ?_⟩ 120 · intro c 121 exact (liftedCornerExponential_commute_stage n h2 heh2 hhe2 c).mul_right 122 (liftedCornerExponential_commute_stage n h1 heh1 hhe1 c) 123 · refine ⟨liftedCornerExponentialPairPath n h1 h2 heh1 hhe1 heh2 hhe2, ?_⟩ 124 intro t c 125 exact liftedCornerExponentialPairPath_commute_stage 126 n h1 h2 heh1 hhe1 heh2 hhe2 t c 127 · intro i 128 have hu2unit : rho (u2 : Limit) ∈ unitary (H →L[ℂ] H) := 129 Unitary.map_mem rho u2.property 130 change ‖rho ((u2 : Limit) * (u1 : Limit)) (v i : H) - (w i : H)‖ < tau 131 rw [map_mul, mul_apply_eq_comp, hu1exact i] 132 have hdecomp : 133 rho (u2 : Limit) (U1 (v i) : H) - (w i : H) = 134 rho (u2 : Limit) ((U1 (v i) : H) - (z i : H)) + 135 (rho (u2 : Limit) (z i : H) - (w i : H)) := by 136 rw [map_sub] 137 module 138 rw [hdecomp] 139 calc 140 _ ≤ ‖rho (u2 : Limit) ((U1 (v i) : H) - (z i : H))‖ + 141 ‖rho (u2 : Limit) (z i : H) - (w i : H)‖ := norm_add_le _ _ 142 _ = ‖(U1 (v i) : H) - (z i : H)‖ + 143 ‖(U2 (z i) : H) - (w i : H)‖ := by 144 rw [(rho (u2 : Limit)).norm_map_of_mem_unitary hu2unit, 145 hu2exact i] 146 _ < tau / 2 + tau / 2 := add_lt_add (hU1 i) (hU2 i) 147 _ = tau := by ring 148 149set_option maxHeartbeats 1000000 in 150/-- Compatibility form of finite-corner local transport, retaining the 151endpoint statement while the stronger theorem also returns its canonical 152all-time stage-central path. -/ 153theorem exists_delta_liftedCornerUnitary_apply_sub_norm_lt 154 {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] 155 [CompleteSpace H] [Nontrivial H] 156 (rho : Representation Limit H) (hrho : StarAlgHom.IsIrreducible rho) 157 (n d : ℕ) {tau : ℝ} (htau : 0 < tau) : 158 ∃ delta > 0, 159 ∀ (v w : Fin d → rootCornerSubspace rho n), 160 (∑ i, ‖v i‖ ^ 2) ≤ 1 → (∑ i, ‖w i‖ ^ 2) ≤ 1 → 161 (∀ i j, ‖inner ℂ (v i) (v j) - inner ℂ (w i) (w j)‖ < delta) → 162 ∃ u : unitary Limit, 163 (∀ c : Stage n, Commute (ofStage n c) (u : Limit)) ∧ 164 ∀ i, ‖rho (u : Limit) (v i : H) - (w i : H)‖ < tau := by 165 obtain ⟨delta, hdelta, hmain⟩ := 166 exists_delta_liftedCornerUnitary_path_apply_sub_norm_lt 167 rho hrho n d htau 168 refine ⟨delta, hdelta, ?_⟩ 169 intro v w hv hw hgram 170 obtain ⟨u, hcomm, -, hmove⟩ := hmain v w hv hw hgram 171 exact ⟨u, hcomm, hmove⟩ 172 173set_option maxHeartbeats 800000 in 174/-- Entrywise closeness of the two vector states on one full CAR stage gives 175an ambient unitary which centralizes that stage and moves the first vector 176close to the second. The modulus is fixed before the vectors. -/ 177theorem exists_delta_stageCentral_unitary_path_apply_sub_norm_lt 178 {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] 179 [CompleteSpace H] [Nontrivial H] 180 (rho : Representation Limit H) (hrho : StarAlgHom.IsIrreducible rho) 181 (n : ℕ) {tau : ℝ} (htau : 0 < tau) : 182 ∃ delta > 0, ∀ (xi eta : H), ‖xi‖ = 1 → ‖eta‖ = 1 → 183 (∀ i j : Fin (2 ^ n), 184 ‖Representation.vectorFunctional rho xi (limitMatrixUnit n i j) - 185 Representation.vectorFunctional rho eta (limitMatrixUnit n i j)‖ < delta) → 186 ∃ u : unitary Limit, 187 (∀ c : Stage n, Commute (ofStage n c) (u : Limit)) ∧ 188 (∃ p : Path 1 u, ∀ t c, 189 Commute (ofStage n c) (p t : Limit)) ∧ 190 ‖rho (u : Limit) xi - eta‖ < tau := by 191 obtain ⟨delta, hdelta, hmain⟩ := 192 exists_delta_liftedCornerUnitary_path_apply_sub_norm_lt 193 rho hrho n (2 ^ n) (div_pos htau (by positivity : (0 : ℝ) < 2 ^ n)) 194 refine ⟨delta, hdelta, ?_⟩ 195 intro xi eta hxi heta hstate 196 let v : Fin (2 ^ n) → rootCornerSubspace rho n := fun i => 197 ⟨rho (limitMatrixUnit n 0 i) xi, by 198 refine ⟨rho (limitMatrixUnit n 0 i) xi, ?_⟩ 199 change (rho (limitMatrixUnit n 0 0) * 200 rho (limitMatrixUnit n 0 i)) xi = _ 201 rw [← map_mul] 202 simp⟩ 203 let w : Fin (2 ^ n) → rootCornerSubspace rho n := fun i => 204 ⟨rho (limitMatrixUnit n 0 i) eta, by 205 refine ⟨rho (limitMatrixUnit n 0 i) eta, ?_⟩ 206 change (rho (limitMatrixUnit n 0 0) * 207 rho (limitMatrixUnit n 0 i)) eta = _ 208 rw [← map_mul] 209 simp⟩ 210 have hvsum : (∑ i, ‖v i‖ ^ 2) ≤ 1 := by 211 have hv := sum_norm_sq_map_limitMatrixUnit_star rho n xi 212 rw [hxi] at hv 213 simpa [v] using hv.le 214 have hwsum : (∑ i, ‖w i‖ ^ 2) ≤ 1 := by 215 have hw := sum_norm_sq_map_limitMatrixUnit_star rho n eta 216 rw [heta] at hw 217 simpa [w] using hw.le 218 obtain ⟨u, hcomm, hpath, hmove⟩ := hmain v w hvsum hwsum (by 219 intro i j 220 change ‖inner ℂ (rho (limitMatrixUnit n 0 i) xi) 221 (rho (limitMatrixUnit n 0 j) xi) - 222 inner ℂ (rho (limitMatrixUnit n 0 i) eta) 223 (rho (limitMatrixUnit n 0 j) eta)‖ < delta 224 rw [show inner ℂ (rho (limitMatrixUnit n 0 i) xi) 225 (rho (limitMatrixUnit n 0 j) xi) = 226 Representation.vectorFunctional rho xi (limitMatrixUnit n i j) by 227 simpa using Representation.inner_map_star_apply rho xi 228 (limitMatrixUnit n i 0) (limitMatrixUnit n j 0)] 229 rw [show inner ℂ (rho (limitMatrixUnit n 0 i) eta) 230 (rho (limitMatrixUnit n 0 j) eta) = 231 Representation.vectorFunctional rho eta (limitMatrixUnit n i j) by 232 simpa using Representation.inner_map_star_apply rho eta 233 (limitMatrixUnit n i 0) (limitMatrixUnit n j 0)] 234 exact hstate i j) 235 refine ⟨u, hcomm, hpath, ?_⟩ 236 have hxiDecomp : 237 xi = ∑ i : Fin (2 ^ n), 238 rho (limitMatrixUnit n i 0) (v i : H) := by 239 calc 240 xi = rho 1 xi := by simp 241 _ = rho (∑ i : Fin (2 ^ n), limitMatrixUnit n i i) xi := by 242 rw [sum_limitMatrixUnit_diag] 243 _ = ∑ i : Fin (2 ^ n), rho (limitMatrixUnit n i i) xi := by 244 rw [map_sum] 245 let ev : (H →L[ℂ] H) →+ H := 246 { toFun := fun T => T xi 247 map_zero' := by simp 248 map_add' := by intro S T; simp } 249 exact map_sum ev _ _ 250 _ = ∑ i : Fin (2 ^ n), 251 rho (limitMatrixUnit n i 0) (v i : H) := by 252 apply Finset.sum_congr rfl 253 intro i _ 254 change rho (limitMatrixUnit n i i) xi = 255 rho (limitMatrixUnit n i 0) (rho (limitMatrixUnit n 0 i) xi) 256 rw [← mul_apply_eq_comp, ← map_mul] 257 simp 258 have hetaDecomp : 259 eta = ∑ i : Fin (2 ^ n), 260 rho (limitMatrixUnit n i 0) (w i : H) := by 261 calc 262 eta = rho 1 eta := by simp 263 _ = rho (∑ i : Fin (2 ^ n), limitMatrixUnit n i i) eta := by 264 rw [sum_limitMatrixUnit_diag] 265 _ = ∑ i : Fin (2 ^ n), rho (limitMatrixUnit n i i) eta := by 266 rw [map_sum] 267 let ev : (H →L[ℂ] H) →+ H := 268 { toFun := fun T => T eta 269 map_zero' := by simp 270 map_add' := by intro S T; simp } 271 exact map_sum ev _ _ 272 _ = ∑ i : Fin (2 ^ n), 273 rho (limitMatrixUnit n i 0) (w i : H) := by 274 apply Finset.sum_congr rfl 275 intro i _ 276 change rho (limitMatrixUnit n i i) eta = 277 rho (limitMatrixUnit n i 0) (rho (limitMatrixUnit n 0 i) eta) 278 rw [← mul_apply_eq_comp, ← map_mul] 279 simp 280 have haction : 281 rho (u : Limit) xi - eta = 282 ∑ i : Fin (2 ^ n), rho (limitMatrixUnit n i 0) 283 (rho (u : Limit) (v i : H) - (w i : H)) := by 284 rw [hxiDecomp, hetaDecomp, map_sum] 285 rw [← Finset.sum_sub_distrib] 286 apply Finset.sum_congr rfl 287 intro i _ 288 rw [map_sub] 289 have hc := (hcomm (matrixUnit n i 0)).map rho 290 have hcapp := congrArg (fun T : H →L[ℂ] H => T (v i : H)) hc.eq 291 simpa [limitMatrixUnit, mul_apply_eq_comp] using hcapp.symm 292 have hmatrixNorm (i : Fin (2 ^ n)) : 293 ‖rho (limitMatrixUnit n i 0)‖ ≤ 1 := by 294 have hsquare : 295 ‖rho (limitMatrixUnit n i 0)‖ * ‖rho (limitMatrixUnit n i 0)‖ = 296 ‖rho (limitMatrixUnit n 0 0)‖ := by 297 rw [← CStarRing.norm_star_mul_self, ← map_star, ← map_mul] 298 simp 299 have hproj := IsStarProjection.norm_le (rho (limitMatrixUnit n 0 0)) 300 ((isStarProjection_limitMatrixUnit_zero_zero n).map rho) 301 nlinarith [norm_nonneg (rho (limitMatrixUnit n i 0))] 302 rw [haction] 303 calc 304 _ ≤ ∑ i : Fin (2 ^ n), 305 ‖rho (limitMatrixUnit n i 0) 306 (rho (u : Limit) (v i : H) - (w i : H))‖ := norm_sum_le _ _ 307 _ ≤ ∑ i : Fin (2 ^ n), 308 ‖rho (u : Limit) (v i : H) - (w i : H)‖ := by 309 apply Finset.sum_le_sum 310 intro i _ 311 calc 312 _ ≤ ‖rho (limitMatrixUnit n i 0)‖ * 313 ‖rho (u : Limit) (v i : H) - (w i : H)‖ := 314 (rho (limitMatrixUnit n i 0)).le_opNorm _ 315 _ ≤ 1 * ‖rho (u : Limit) (v i : H) - (w i : H)‖ := by 316 gcongr 317 exact hmatrixNorm i 318 _ = _ := one_mul _ 319 _ < ∑ _i : Fin (2 ^ n), tau / (2 ^ n : ℝ) := by 320 apply Finset.sum_lt_sum_of_nonempty Finset.univ_nonempty 321 intro i _ 322 exact hmove i 323 _ = tau := by 324 simp only [Finset.sum_const, Finset.card_fin, nsmul_eq_mul] 325 field_simp 326 norm_cast 327 328set_option maxHeartbeats 800000 in 329/-- Compatibility endpoint for stage-central transport. The strengthened 330form above additionally retains an explicit path which is exactly 331stage-central at every time. -/ 332theorem exists_delta_stageCentral_unitary_apply_sub_norm_lt 333 {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] 334 [CompleteSpace H] [Nontrivial H] 335 (rho : Representation Limit H) (hrho : StarAlgHom.IsIrreducible rho) 336 (n : ℕ) {tau : ℝ} (htau : 0 < tau) : 337 ∃ delta > 0, ∀ (xi eta : H), ‖xi‖ = 1 → ‖eta‖ = 1 → 338 (∀ i j : Fin (2 ^ n), 339 ‖Representation.vectorFunctional rho xi (limitMatrixUnit n i j) - 340 Representation.vectorFunctional rho eta (limitMatrixUnit n i j)‖ < delta) → 341 ∃ u : unitary Limit, 342 (∀ c : Stage n, Commute (ofStage n c) (u : Limit)) ∧ 343 ‖rho (u : Limit) xi - eta‖ < tau := by 344 obtain ⟨delta, hdelta, hmain⟩ := 345 exists_delta_stageCentral_unitary_path_apply_sub_norm_lt 346 rho hrho n htau 347 refine ⟨delta, hdelta, ?_⟩ 348 intro xi eta hxi heta hstate 349 obtain ⟨u, hcomm, -, hmove⟩ := hmain xi eta hxi heta hstate 350 exact ⟨u, hcomm, hmove⟩ 351 352set_option maxHeartbeats 800000 in 353/-- Once a stage is fixed, entrywise closeness of two unit vector states on 354that stage gives an exact vector transport. The implementing unitary has a 355commutator bound on the whole stage. The exact correction is made after a 356stage-central finite-corner transport, so its modulus is chosen before the 357vectors. -/ 358theorem exists_delta_exact_unitary_path_apply_eq_and_stage_commutator 359 {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] 360 [CompleteSpace H] [Nontrivial H] 361 (rho : Representation Limit H) (hrho : StarAlgHom.IsIrreducible rho) 362 (n : ℕ) {epsilon : ℝ} (hepsilon : 0 < epsilon) : 363 ∃ delta > 0, ∀ (xi eta : H), ‖xi‖ = 1 → ‖eta‖ = 1 → 364 (∀ i j : Fin (2 ^ n), 365 ‖Representation.vectorFunctional rho xi (limitMatrixUnit n i j) - 366 Representation.vectorFunctional rho eta (limitMatrixUnit n i j)‖ < delta) → 367 ∃ u : unitary Limit, 368 rho (u : Limit) xi = eta ∧ 369 ∃ p : Path 1 u, ∀ t c, 370 ‖(p t : Limit) * ofStage n c - ofStage n c * (p t : Limit)‖ ≤ 371 epsilon * ‖ofStage n c‖ := by 372 let epsilon0 : ℝ := min (epsilon / 2) 1 373 have hepsilon0 : 0 < epsilon0 := by 374 dsimp only [epsilon0] 375 positivity 376 obtain ⟨tau, htau, hsmall⟩ := 377 StarAlgHom.exists_unitary_apply_eq_and_norm_sub_one_lt 378 rho hrho hepsilon0 379 obtain ⟨delta, hdelta, hstage⟩ := 380 exists_delta_stageCentral_unitary_path_apply_sub_norm_lt rho hrho n htau 381 refine ⟨delta, hdelta, ?_⟩ 382 intro xi eta hxi heta hstate 383 obtain ⟨u0, hcentral, ⟨p0, hp0⟩, hclose⟩ := 384 hstage xi eta hxi heta hstate 385 have hu0map : rho (u0 : Limit) ∈ unitary (H →L[ℂ] H) := 386 Unitary.map_mem rho u0.property 387 have hzeta : ‖rho (u0 : Limit) xi‖ = 1 := by 388 rw [(rho (u0 : Limit)).norm_map_of_mem_unitary hu0map, hxi] 389 obtain ⟨v, hvapply, hvnorm⟩ := 390 hsmall (rho (u0 : Limit) xi) eta hzeta heta hclose 391 have hvhalf : ‖(v : Limit) - 1‖ < epsilon / 2 := 392 hvnorm.trans_le (min_le_left _ _) 393 have hvTwo : ‖(v : Limit) - 1‖ < 2 := by 394 calc 395 _ < 1 := hvnorm.trans_le (min_le_right _ _) 396 _ < 2 := by norm_num 397 let pv : Path (1 : unitary Limit) v := Unitary.path 1 v (by 398 simpa using hvTwo) 399 let u : unitary Limit := v * u0 400 let q : Path u0 u := 401 { toFun := fun t => pv t * u0 402 continuous_toFun := by fun_prop 403 source' := by rw [pv.source]; simp 404 target' := by rw [pv.target] } 405 let p : Path 1 u := p0.trans q 406 refine ⟨u, ?_, p, ?_⟩ 407 · change rho ((v : Limit) * (u0 : Limit)) xi = eta 408 rw [map_mul, mul_apply_eq_comp, hvapply] 409 · have hp0bound (t : Set.Icc (0 : ℝ) 1) (c : Stage n) : 410 ‖(p0 t : Limit) * ofStage n c - 411 ofStage n c * (p0 t : Limit)‖ ≤ 412 epsilon * ‖ofStage n c‖ := by 413 rw [(hp0 t c).eq] 414 simp only [sub_self, norm_zero] 415 positivity 416 have hqbound (t : Set.Icc (0 : ℝ) 1) (c : Stage n) : 417 ‖(q t : Limit) * ofStage n c - 418 ofStage n c * (q t : Limit)‖ ≤ 419 epsilon * ‖ofStage n c‖ := by 420 have hpvnorm : ‖(pv t : Limit) - 1‖ ≤ ‖(v : Limit) - 1‖ := by 421 have h := Unitary.norm_expUnitary_smul_argSelfAdjoint_sub_one_le 422 v t.2 hvTwo 423 simpa [pv, Unitary.path] using h 424 have hcommEq : 425 (q t : Limit) * ofStage n c - ofStage n c * (q t : Limit) = 426 (((pv t : Limit) - 1) * ofStage n c - 427 ofStage n c * ((pv t : Limit) - 1)) * (u0 : Limit) := by 428 change (((pv t : unitary Limit) * u0 : unitary Limit) : Limit) * 429 ofStage n c - ofStage n c * 430 ((((pv t : unitary Limit) * u0 : unitary Limit) : Limit)) = _ 431 simp only [Submonoid.coe_mul] 432 noncomm_ring [(hcentral c).eq] 433 rw [hcommEq, CStarRing.norm_mul_coe_unitary] 434 calc 435 _ ≤ ‖((pv t : Limit) - 1) * ofStage n c‖ + 436 ‖ofStage n c * ((pv t : Limit) - 1)‖ := norm_sub_le _ _ 437 _ ≤ ‖(pv t : Limit) - 1‖ * ‖ofStage n c‖ + 438 ‖ofStage n c‖ * ‖(pv t : Limit) - 1‖ := by 439 exact add_le_add (norm_mul_le _ _) (norm_mul_le _ _) 440 _ = 2 * ‖(pv t : Limit) - 1‖ * ‖ofStage n c‖ := by ring 441 _ ≤ 2 * ‖(v : Limit) - 1‖ * ‖ofStage n c‖ := by 442 gcongr 443 _ ≤ epsilon * ‖ofStage n c‖ := by 444 have hmul := mul_le_mul_of_nonneg_right hvhalf.le 445 (norm_nonneg (ofStage n c)) 446 nlinarith 447 intro t c 448 have ht : p t ∈ Set.range p0 ∪ Set.range q := by 449 rw [← Path.trans_range] 450 exact ⟨t, rfl⟩ 451 rcases ht with ⟨s, hs⟩ | ⟨s, hs⟩ 452 · rw [show p t = p0 s by exact hs.symm] 453 exact hp0bound s c 454 · rw [show p t = q s by exact hs.symm] 455 exact hqbound s c 456 457set_option maxHeartbeats 800000 in 458/-- Endpoint compatibility form of exact stage transport. The stronger 459theorem above supplies a path with the same commutator bound at every time. -/ 460theorem exists_delta_exact_unitary_apply_eq_and_stage_commutator 461 {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] 462 [CompleteSpace H] [Nontrivial H] 463 (rho : Representation Limit H) (hrho : StarAlgHom.IsIrreducible rho) 464 (n : ℕ) {epsilon : ℝ} (hepsilon : 0 < epsilon) : 465 ∃ delta > 0, ∀ (xi eta : H), ‖xi‖ = 1 → ‖eta‖ = 1 → 466 (∀ i j : Fin (2 ^ n), 467 ‖Representation.vectorFunctional rho xi (limitMatrixUnit n i j) - 468 Representation.vectorFunctional rho eta (limitMatrixUnit n i j)‖ < delta) → 469 ∃ u : unitary Limit, 470 rho (u : Limit) xi = eta ∧ 471 ∀ c : Stage n, 472 ‖(u : Limit) * ofStage n c - ofStage n c * (u : Limit)‖ ≤ 473 epsilon * ‖ofStage n c‖ := by 474 obtain ⟨delta, hdelta, hmain⟩ := 475 exists_delta_exact_unitary_path_apply_eq_and_stage_commutator 476 rho hrho n hepsilon 477 refine ⟨delta, hdelta, ?_⟩ 478 intro xi eta hxi heta hstate 479 obtain ⟨u, huapply, p, hp⟩ := hmain xi eta hxi heta hstate 480 refine ⟨u, huapply, ?_⟩ 481 intro c 482 have h := hp (1 : Set.Icc (0 : ℝ) 1) c 483 simpa only [p.target] using h 484 485set_option maxHeartbeats 800000 in 486/-- Local exact transport in path form for the alternating construction. 487For a prescribed finite set, one stage and one entrywise state tolerance are 488fixed first. Any two unit vectors meeting those tests are related exactly by 489an inner unitary, along a path whose forward and inverse conjugations are 490uniformly small on the prescribed set at every time. -/ 491theorem exists_stageTests_exact_unitary_path_apply_eq_and_conjugate_sub_norm_lt 492 {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] 493 [CompleteSpace H] [Nontrivial H] 494 (rho : Representation Limit H) (hrho : StarAlgHom.IsIrreducible rho) 495 (F : Finset Limit) {epsilon : ℝ} (hepsilon : 0 < epsilon) : 496 ∃ n, ∃ delta > 0, ∀ (xi eta : H), ‖xi‖ = 1 → ‖eta‖ = 1 → 497 (∀ i j : Fin (2 ^ n), 498 ‖Representation.vectorFunctional rho xi (limitMatrixUnit n i j) - 499 Representation.vectorFunctional rho eta (limitMatrixUnit n i j)‖ < delta) → 500 ∃ u : unitary Limit, 501 rho (u : Limit) xi = eta ∧ 502 ∃ p : Path 1 u, ∀ t, ∀ a ∈ F, 503 ‖(p t : Limit) * a * star (p t : Limit) - a‖ < epsilon ∧ 504 ‖star (p t : Limit) * a * (p t : Limit) - a‖ < epsilon := by 505 classical 506 let M : ℝ := (∑ a ∈ F, ‖a‖) + epsilon / 8 + 1 507 have hsum : 0 ≤ ∑ a ∈ F, ‖a‖ := Finset.sum_nonneg (fun _ _ => norm_nonneg _) 508 have hM : 0 < M := by 509 dsimp only [M] 510 linarith 511 obtain ⟨n, hn⟩ := exists_common_stage_approx F 512 (show 0 < epsilon / 8 by positivity) 513 let gamma : ℝ := epsilon / (4 * M) 514 have hgamma : 0 < gamma := by 515 dsimp only [gamma] 516 positivity 517 obtain ⟨delta, hdelta, hlocal⟩ := 518 exists_delta_exact_unitary_path_apply_eq_and_stage_commutator 519 rho hrho n hgamma 520 refine ⟨n, delta, hdelta, ?_⟩ 521 intro xi eta hxi heta hstate 522 obtain ⟨u, huapply, p, hcomm⟩ := hlocal xi eta hxi heta hstate 523 refine ⟨u, huapply, p, ?_⟩ 524 intro t a ha 525 let ut : unitary Limit := p t 526 obtain ⟨c, hc⟩ := hn a ha 527 have haSum : ‖a‖ ≤ ∑ x ∈ F, ‖x‖ := 528 Finset.single_le_sum (fun x _ => norm_nonneg x) ha 529 have hcM : ‖ofStage n c‖ < M := by 530 calc 531 ‖ofStage n c‖ = ‖a - (a - ofStage n c)‖ := by 532 congr 1 533 module 534 _ ≤ ‖a‖ + ‖a - ofStage n c‖ := norm_sub_le _ _ 535 _ < ‖a‖ + epsilon / 8 := by linarith 536 _ ≤ (∑ x ∈ F, ‖x‖) + epsilon / 8 := by 537 simpa only [add_comm] using add_le_add_right haSum (epsilon / 8) 538 _ < M := by dsimp only [M]; linarith 539 have hgammaM : gamma * ‖ofStage n c‖ < epsilon / 4 := by 540 calc 541 _ < gamma * M := mul_lt_mul_of_pos_left hcM hgamma 542 _ = epsilon / 4 := by 543 dsimp only [gamma] 544 field_simp 545 have hcommA : 546 ‖(ut : Limit) * a - a * (ut : Limit)‖ < epsilon := by 547 have hdecomp : 548 (ut : Limit) * a - a * (ut : Limit) = 549 (ut : Limit) * (a - ofStage n c) + 550 ((ut : Limit) * ofStage n c - ofStage n c * (ut : Limit)) + 551 (ofStage n c - a) * (ut : Limit) := by noncomm_ring 552 rw [hdecomp] 553 calc 554 _ ≤ ‖(ut : Limit) * (a - ofStage n c)‖ + 555 ‖(ut : Limit) * ofStage n c - ofStage n c * (ut : Limit)‖ + 556 ‖(ofStage n c - a) * (ut : Limit)‖ := by 557 exact (norm_add_le _ _).trans 558 (add_le_add_left (norm_add_le _ _) _) 559 _ = ‖a - ofStage n c‖ + 560 ‖(ut : Limit) * ofStage n c - ofStage n c * (ut : Limit)‖ + 561 ‖ofStage n c - a‖ := by 562 rw [CStarRing.norm_coe_unitary_mul, CStarRing.norm_mul_coe_unitary] 563 _ ≤ ‖a - ofStage n c‖ + gamma * ‖ofStage n c‖ + 564 ‖ofStage n c - a‖ := by 565 gcongr 566 exact hcomm t c 567 _ < epsilon := by 568 rw [norm_sub_rev (ofStage n c) a] 569 nlinarith 570 have hconj : 571 (ut : Limit) * a * star (ut : Limit) - a = 572 ((ut : Limit) * a - a * (ut : Limit)) * star (ut : Limit) := by 573 symm 574 calc 575 ((ut : Limit) * a - a * (ut : Limit)) * star (ut : Limit) = 576 ((ut : Limit) * a) * star (ut : Limit) - 577 (a * (ut : Limit)) * star (ut : Limit) := sub_mul _ _ _ 578 _ = (ut : Limit) * a * star (ut : Limit) - a := by 579 have huunit : (ut : Limit) * star (ut : Limit) = 1 := 580 Unitary.mul_star_self_of_mem ut.property 581 rw [mul_assoc a (ut : Limit) (star (ut : Limit)), huunit, mul_one] 582 constructor 583 · rw [hconj] 584 have hstar : star (ut : Limit) = ((star ut : unitary Limit) : Limit) := rfl 585 rw [hstar, CStarRing.norm_mul_coe_unitary] 586 exact hcommA 587 · have hconjInv : 588 star (ut : Limit) * a * (ut : Limit) - a = 589 star (ut : Limit) * (a * (ut : Limit) - (ut : Limit) * a) := by 590 have huunit : star (ut : Limit) * (ut : Limit) = 1 := 591 Unitary.star_mul_self_of_mem ut.property 592 symm 593 calc 594 star (ut : Limit) * (a * (ut : Limit) - (ut : Limit) * a) = 595 star (ut : Limit) * (a * (ut : Limit)) - 596 star (ut : Limit) * ((ut : Limit) * a) := mul_sub _ _ _ 597 _ = (star (ut : Limit) * a) * (ut : Limit) - 598 (star (ut : Limit) * (ut : Limit)) * a := by 599 rw [mul_assoc, mul_assoc] 600 _ = star (ut : Limit) * a * (ut : Limit) - a := by 601 rw [huunit, one_mul] 602 rw [hconjInv] 603 have hstar : star (ut : Limit) = ((star ut : unitary Limit) : Limit) := rfl 604 rw [hstar, CStarRing.norm_coe_unitary_mul] 605 rw [show a * (ut : Limit) - (ut : Limit) * a = 606 -((ut : Limit) * a - a * (ut : Limit)) by module, norm_neg] 607 exact hcommA 608 609set_option maxHeartbeats 800000 in 610/-- Endpoint compatibility form of finite-set exact local transport. -/ 611theorem exists_stageTests_exact_unitary_apply_eq_and_conjugate_sub_norm_lt 612 {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] 613 [CompleteSpace H] [Nontrivial H] 614 (rho : Representation Limit H) (hrho : StarAlgHom.IsIrreducible rho) 615 (F : Finset Limit) {epsilon : ℝ} (hepsilon : 0 < epsilon) : 616 ∃ n, ∃ delta > 0, ∀ (xi eta : H), ‖xi‖ = 1 → ‖eta‖ = 1 → 617 (∀ i j : Fin (2 ^ n), 618 ‖Representation.vectorFunctional rho xi (limitMatrixUnit n i j) - 619 Representation.vectorFunctional rho eta (limitMatrixUnit n i j)‖ < delta) → 620 ∃ u : unitary Limit, 621 rho (u : Limit) xi = eta ∧ 622 ∀ a ∈ F, 623 ‖(u : Limit) * a * star (u : Limit) - a‖ < epsilon ∧ 624 ‖star (u : Limit) * a * (u : Limit) - a‖ < epsilon := by 625 obtain ⟨n, delta, hdelta, hmain⟩ := 626 exists_stageTests_exact_unitary_path_apply_eq_and_conjugate_sub_norm_lt 627 rho hrho F hepsilon 628 refine ⟨n, delta, hdelta, ?_⟩ 629 intro xi eta hxi heta hstate 630 obtain ⟨u, huapply, p, hp⟩ := hmain xi eta hxi heta hstate 631 refine ⟨u, huapply, ?_⟩ 632 intro a ha 633 have h := hp (1 : Set.Icc (0 : ℝ) 1) a ha 634 simpa only [p.target] using h 635 636end MathlibAnnex.CStarAlgebra.CAR