Exact source: MathlibAnnex/Analysis/CStarAlgebra/CAR/LocalTransport.lean
Pinned GitHub source · Raw UTF-8 source
Back to Exact vector transport along an almost central unitary path
1import MathlibAnnex.Analysis.CStarAlgebra.CAR.InvolutionLift2import MathlibAnnex.Analysis.InnerProductSpace.GramPerturbation3import MathlibAnnex.Analysis.InnerProductSpace.FiniteEmbedding45set_option autoImplicit false67noncomputable section89open MathlibAnnex.Analysis.CStarAlgebra10open MathlibAnnex.Analysis.InnerProductSpace11open MathlibAnnex.InnerProductSpace1213namespace MathlibAnnex.CStarAlgebra.CAR1415set_option maxHeartbeats 1000000 in16theorem exists_delta_liftedCornerUnitary_path_apply_sub_norm_lt17 {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 := by30 obtain ⟨delta, hdelta, hperturb⟩ :=31 exists_delta_orthogonalGramPerturbation (n := d) (half_pos htau)32 refine ⟨delta, hdelta, ?_⟩33 intro v w hv hw hgram34 let e : Limit := limitMatrixUnit n 0 035 let K : Submodule ℂ H := rootCornerSubspace rho n36 have hroot : IsStarProjection (rho e) :=37 (isStarProjection_limitMatrixUnit_zero_zero n).map rho38 letI : CompleteSpace K := IsComplete.completeSpace_coe39 (ContinuousLinearMap.IsIdempotentElem.isClosed_range40 hroot.isIdempotentElem).isComplete41 have hKnot : ¬ FiniteDimensional ℂ K := by42 simpa [K, e, rootCornerSubspace] using43 not_finiteDimensional_range_rootCorner rho44 ((Representation.isIrreducible_iff_starAlgHom rho).mpr hrho) n45 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 := inferInstance51 let R : Submodule ℂ K := Vᗮ52 letI : CompleteSpace R := IsComplete.completeSpace_coe53 (show IsClosed (R : Set K) by54 simpa [R] using Submodule.isClosed_orthogonal V).isComplete55 have hRnot : ¬ FiniteDimensional ℂ R := by56 intro hR57 letI : FiniteDimensional ℂ R := hR58 have htop : V ⊔ R = ⊤ := by59 simpa [R] using60 (Submodule.sup_orthogonal_of_hasOrthogonalProjection (K := V))61 letI : FiniteDimensional ℂ (V ⊔ R : Submodule ℂ K) := inferInstance62 apply hKnot63 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_finiteDimensional70 (E := S) (F := R) hRnot71 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)).property79 have hzgram (i j : Fin d) :80 inner ℂ (z i) (z j) = inner ℂ (v i) (v j) := by81 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 := by84 calc85 (∑ i, ‖z i‖ ^ 2) = ∑ i, ‖v i‖ ^ 2 := by86 apply Finset.sum_congr rfl87 intro i _88 rw [show ‖z i‖ = ‖v i‖ by exact L.norm_map (vS i)]89 _ ≤ 1 := hv90 have hvzorth : ∀ i j, inner ℂ (v i) (z j) = 0 := by91 intro i j92 exact V.inner_right_of_mem_orthogonal (hvV i) (hzR j)93 have hzworth : ∀ i j, inner ℂ (z i) (w j) = 0 := by94 intro i j95 exact V.inner_left_of_mem_orthogonal (hwV j) (hzR i)96 obtain ⟨U1, hU1, -, hU1sq, hU1finite⟩ :=97 hperturb v z hv hzsum hvzorth (by98 intro i j99 rw [hzgram]100 simpa using hdelta)101 obtain ⟨U2, hU2, -, hU2sq, hU2finite⟩ :=102 hperturb z w hzsum hw hzworth (by103 intro i j104 rw [hzgram]105 exact hgram i j)106 letI : FiniteDimensional ℂ107 (LinearMap.range (U1.toLinearMap - LinearMap.id)) := hU1finite108 obtain ⟨h1, heh1, hhe1, hu1exact⟩ :=109 exists_liftedCornerExponential_apply_eq_involution110 rho hrho n d v U1 hU1sq111 letI : FiniteDimensional ℂ112 (LinearMap.range (U2.toLinearMap - LinearMap.id)) := hU2finite113 obtain ⟨h2, heh2, hhe2, hu2exact⟩ :=114 exists_liftedCornerExponential_apply_eq_involution115 rho hrho n d z U2 hU2sq116 let u1 : unitary Limit := liftedCornerExponential n h1 heh1 hhe1117 let u2 : unitary Limit := liftedCornerExponential n h2 heh2 hhe2118 let u : unitary Limit := u2 * u1119 refine ⟨u, ?_, ?_, ?_⟩120 · intro c121 exact (liftedCornerExponential_commute_stage n h2 heh2 hhe2 c).mul_right122 (liftedCornerExponential_commute_stage n h1 heh1 hhe1 c)123 · refine ⟨liftedCornerExponentialPairPath n h1 h2 heh1 hhe1 heh2 hhe2, ?_⟩124 intro t c125 exact liftedCornerExponentialPairPath_commute_stage126 n h1 h2 heh1 hhe1 heh2 hhe2 t c127 · intro i128 have hu2unit : rho (u2 : Limit) ∈ unitary (H →L[ℂ] H) :=129 Unitary.map_mem rho u2.property130 change ‖rho ((u2 : Limit) * (u1 : Limit)) (v i : H) - (w i : H)‖ < tau131 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)) := by136 rw [map_sub]137 module138 rw [hdecomp]139 calc140 _ ≤ ‖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)‖ := by144 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 ring148149set_option maxHeartbeats 1000000 in150/-- Compatibility form of finite-corner local transport, retaining the151endpoint statement while the stronger theorem also returns its canonical152all-time stage-central path. -/153theorem exists_delta_liftedCornerUnitary_apply_sub_norm_lt154 {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 := by165 obtain ⟨delta, hdelta, hmain⟩ :=166 exists_delta_liftedCornerUnitary_path_apply_sub_norm_lt167 rho hrho n d htau168 refine ⟨delta, hdelta, ?_⟩169 intro v w hv hw hgram170 obtain ⟨u, hcomm, -, hmove⟩ := hmain v w hv hw hgram171 exact ⟨u, hcomm, hmove⟩172173set_option maxHeartbeats 800000 in174/-- Entrywise closeness of the two vector states on one full CAR stage gives175an ambient unitary which centralizes that stage and moves the first vector176close to the second. The modulus is fixed before the vectors. -/177theorem exists_delta_stageCentral_unitary_path_apply_sub_norm_lt178 {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 := by191 obtain ⟨delta, hdelta, hmain⟩ :=192 exists_delta_liftedCornerUnitary_path_apply_sub_norm_lt193 rho hrho n (2 ^ n) (div_pos htau (by positivity : (0 : ℝ) < 2 ^ n))194 refine ⟨delta, hdelta, ?_⟩195 intro xi eta hxi heta hstate196 let v : Fin (2 ^ n) → rootCornerSubspace rho n := fun i =>197 ⟨rho (limitMatrixUnit n 0 i) xi, by198 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, by205 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 := by211 have hv := sum_norm_sq_map_limitMatrixUnit_star rho n xi212 rw [hxi] at hv213 simpa [v] using hv.le214 have hwsum : (∑ i, ‖w i‖ ^ 2) ≤ 1 := by215 have hw := sum_norm_sq_map_limitMatrixUnit_star rho n eta216 rw [heta] at hw217 simpa [w] using hw.le218 obtain ⟨u, hcomm, hpath, hmove⟩ := hmain v w hvsum hwsum (by219 intro i j220 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)‖ < delta224 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) by227 simpa using Representation.inner_map_star_apply rho xi228 (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) by232 simpa using Representation.inner_map_star_apply rho eta233 (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) := by239 calc240 xi = rho 1 xi := by simp241 _ = rho (∑ i : Fin (2 ^ n), limitMatrixUnit n i i) xi := by242 rw [sum_limitMatrixUnit_diag]243 _ = ∑ i : Fin (2 ^ n), rho (limitMatrixUnit n i i) xi := by244 rw [map_sum]245 let ev : (H →L[ℂ] H) →+ H :=246 { toFun := fun T => T xi247 map_zero' := by simp248 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) := by252 apply Finset.sum_congr rfl253 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 simp258 have hetaDecomp :259 eta = ∑ i : Fin (2 ^ n),260 rho (limitMatrixUnit n i 0) (w i : H) := by261 calc262 eta = rho 1 eta := by simp263 _ = rho (∑ i : Fin (2 ^ n), limitMatrixUnit n i i) eta := by264 rw [sum_limitMatrixUnit_diag]265 _ = ∑ i : Fin (2 ^ n), rho (limitMatrixUnit n i i) eta := by266 rw [map_sum]267 let ev : (H →L[ℂ] H) →+ H :=268 { toFun := fun T => T eta269 map_zero' := by simp270 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) := by274 apply Finset.sum_congr rfl275 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 simp280 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)) := by284 rw [hxiDecomp, hetaDecomp, map_sum]285 rw [← Finset.sum_sub_distrib]286 apply Finset.sum_congr rfl287 intro i _288 rw [map_sub]289 have hc := (hcomm (matrixUnit n i 0)).map rho290 have hcapp := congrArg (fun T : H →L[ℂ] H => T (v i : H)) hc.eq291 simpa [limitMatrixUnit, mul_apply_eq_comp] using hcapp.symm292 have hmatrixNorm (i : Fin (2 ^ n)) :293 ‖rho (limitMatrixUnit n i 0)‖ ≤ 1 := by294 have hsquare :295 ‖rho (limitMatrixUnit n i 0)‖ * ‖rho (limitMatrixUnit n i 0)‖ =296 ‖rho (limitMatrixUnit n 0 0)‖ := by297 rw [← CStarRing.norm_star_mul_self, ← map_star, ← map_mul]298 simp299 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 calc304 _ ≤ ∑ 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)‖ := by309 apply Finset.sum_le_sum310 intro i _311 calc312 _ ≤ ‖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)‖ := by316 gcongr317 exact hmatrixNorm i318 _ = _ := one_mul _319 _ < ∑ _i : Fin (2 ^ n), tau / (2 ^ n : ℝ) := by320 apply Finset.sum_lt_sum_of_nonempty Finset.univ_nonempty321 intro i _322 exact hmove i323 _ = tau := by324 simp only [Finset.sum_const, Finset.card_fin, nsmul_eq_mul]325 field_simp326 norm_cast327328set_option maxHeartbeats 800000 in329/-- Compatibility endpoint for stage-central transport. The strengthened330form above additionally retains an explicit path which is exactly331stage-central at every time. -/332theorem exists_delta_stageCentral_unitary_apply_sub_norm_lt333 {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 := by344 obtain ⟨delta, hdelta, hmain⟩ :=345 exists_delta_stageCentral_unitary_path_apply_sub_norm_lt346 rho hrho n htau347 refine ⟨delta, hdelta, ?_⟩348 intro xi eta hxi heta hstate349 obtain ⟨u, hcomm, -, hmove⟩ := hmain xi eta hxi heta hstate350 exact ⟨u, hcomm, hmove⟩351352set_option maxHeartbeats 800000 in353/-- Once a stage is fixed, entrywise closeness of two unit vector states on354that stage gives an exact vector transport. The implementing unitary has a355commutator bound on the whole stage. The exact correction is made after a356stage-central finite-corner transport, so its modulus is chosen before the357vectors. -/358theorem exists_delta_exact_unitary_path_apply_eq_and_stage_commutator359 {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‖ := by372 let epsilon0 : ℝ := min (epsilon / 2) 1373 have hepsilon0 : 0 < epsilon0 := by374 dsimp only [epsilon0]375 positivity376 obtain ⟨tau, htau, hsmall⟩ :=377 StarAlgHom.exists_unitary_apply_eq_and_norm_sub_one_lt378 rho hrho hepsilon0379 obtain ⟨delta, hdelta, hstage⟩ :=380 exists_delta_stageCentral_unitary_path_apply_sub_norm_lt rho hrho n htau381 refine ⟨delta, hdelta, ?_⟩382 intro xi eta hxi heta hstate383 obtain ⟨u0, hcentral, ⟨p0, hp0⟩, hclose⟩ :=384 hstage xi eta hxi heta hstate385 have hu0map : rho (u0 : Limit) ∈ unitary (H →L[ℂ] H) :=386 Unitary.map_mem rho u0.property387 have hzeta : ‖rho (u0 : Limit) xi‖ = 1 := by388 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 hclose391 have hvhalf : ‖(v : Limit) - 1‖ < epsilon / 2 :=392 hvnorm.trans_le (min_le_left _ _)393 have hvTwo : ‖(v : Limit) - 1‖ < 2 := by394 calc395 _ < 1 := hvnorm.trans_le (min_le_right _ _)396 _ < 2 := by norm_num397 let pv : Path (1 : unitary Limit) v := Unitary.path 1 v (by398 simpa using hvTwo)399 let u : unitary Limit := v * u0400 let q : Path u0 u :=401 { toFun := fun t => pv t * u0402 continuous_toFun := by fun_prop403 source' := by rw [pv.source]; simp404 target' := by rw [pv.target] }405 let p : Path 1 u := p0.trans q406 refine ⟨u, ?_, p, ?_⟩407 · change rho ((v : Limit) * (u0 : Limit)) xi = eta408 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‖ := by413 rw [(hp0 t c).eq]414 simp only [sub_self, norm_zero]415 positivity416 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‖ := by420 have hpvnorm : ‖(pv t : Limit) - 1‖ ≤ ‖(v : Limit) - 1‖ := by421 have h := Unitary.norm_expUnitary_smul_argSelfAdjoint_sub_one_le422 v t.2 hvTwo423 simpa [pv, Unitary.path] using h424 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) := by428 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 calc435 _ ≤ ‖((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‖ := by439 exact add_le_add (norm_mul_le _ _) (norm_mul_le _ _)440 _ = 2 * ‖(pv t : Limit) - 1‖ * ‖ofStage n c‖ := by ring441 _ ≤ 2 * ‖(v : Limit) - 1‖ * ‖ofStage n c‖ := by442 gcongr443 _ ≤ epsilon * ‖ofStage n c‖ := by444 have hmul := mul_le_mul_of_nonneg_right hvhalf.le445 (norm_nonneg (ofStage n c))446 nlinarith447 intro t c448 have ht : p t ∈ Set.range p0 ∪ Set.range q := by449 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 c454 · rw [show p t = q s by exact hs.symm]455 exact hqbound s c456457set_option maxHeartbeats 800000 in458/-- Endpoint compatibility form of exact stage transport. The stronger459theorem above supplies a path with the same commutator bound at every time. -/460theorem exists_delta_exact_unitary_apply_eq_and_stage_commutator461 {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‖ := by474 obtain ⟨delta, hdelta, hmain⟩ :=475 exists_delta_exact_unitary_path_apply_eq_and_stage_commutator476 rho hrho n hepsilon477 refine ⟨delta, hdelta, ?_⟩478 intro xi eta hxi heta hstate479 obtain ⟨u, huapply, p, hp⟩ := hmain xi eta hxi heta hstate480 refine ⟨u, huapply, ?_⟩481 intro c482 have h := hp (1 : Set.Icc (0 : ℝ) 1) c483 simpa only [p.target] using h484485set_option maxHeartbeats 800000 in486/-- Local exact transport in path form for the alternating construction.487For a prescribed finite set, one stage and one entrywise state tolerance are488fixed first. Any two unit vectors meeting those tests are related exactly by489an inner unitary, along a path whose forward and inverse conjugations are490uniformly small on the prescribed set at every time. -/491theorem exists_stageTests_exact_unitary_path_apply_eq_and_conjugate_sub_norm_lt492 {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 := by505 classical506 let M : ℝ := (∑ a ∈ F, ‖a‖) + epsilon / 8 + 1507 have hsum : 0 ≤ ∑ a ∈ F, ‖a‖ := Finset.sum_nonneg (fun _ _ => norm_nonneg _)508 have hM : 0 < M := by509 dsimp only [M]510 linarith511 obtain ⟨n, hn⟩ := exists_common_stage_approx F512 (show 0 < epsilon / 8 by positivity)513 let gamma : ℝ := epsilon / (4 * M)514 have hgamma : 0 < gamma := by515 dsimp only [gamma]516 positivity517 obtain ⟨delta, hdelta, hlocal⟩ :=518 exists_delta_exact_unitary_path_apply_eq_and_stage_commutator519 rho hrho n hgamma520 refine ⟨n, delta, hdelta, ?_⟩521 intro xi eta hxi heta hstate522 obtain ⟨u, huapply, p, hcomm⟩ := hlocal xi eta hxi heta hstate523 refine ⟨u, huapply, p, ?_⟩524 intro t a ha525 let ut : unitary Limit := p t526 obtain ⟨c, hc⟩ := hn a ha527 have haSum : ‖a‖ ≤ ∑ x ∈ F, ‖x‖ :=528 Finset.single_le_sum (fun x _ => norm_nonneg x) ha529 have hcM : ‖ofStage n c‖ < M := by530 calc531 ‖ofStage n c‖ = ‖a - (a - ofStage n c)‖ := by532 congr 1533 module534 _ ≤ ‖a‖ + ‖a - ofStage n c‖ := norm_sub_le _ _535 _ < ‖a‖ + epsilon / 8 := by linarith536 _ ≤ (∑ x ∈ F, ‖x‖) + epsilon / 8 := by537 simpa only [add_comm] using add_le_add_right haSum (epsilon / 8)538 _ < M := by dsimp only [M]; linarith539 have hgammaM : gamma * ‖ofStage n c‖ < epsilon / 4 := by540 calc541 _ < gamma * M := mul_lt_mul_of_pos_left hcM hgamma542 _ = epsilon / 4 := by543 dsimp only [gamma]544 field_simp545 have hcommA :546 ‖(ut : Limit) * a - a * (ut : Limit)‖ < epsilon := by547 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_ring552 rw [hdecomp]553 calc554 _ ≤ ‖(ut : Limit) * (a - ofStage n c)‖ +555 ‖(ut : Limit) * ofStage n c - ofStage n c * (ut : Limit)‖ +556 ‖(ofStage n c - a) * (ut : Limit)‖ := by557 exact (norm_add_le _ _).trans558 (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‖ := by562 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‖ := by565 gcongr566 exact hcomm t c567 _ < epsilon := by568 rw [norm_sub_rev (ofStage n c) a]569 nlinarith570 have hconj :571 (ut : Limit) * a * star (ut : Limit) - a =572 ((ut : Limit) * a - a * (ut : Limit)) * star (ut : Limit) := by573 symm574 calc575 ((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 := by579 have huunit : (ut : Limit) * star (ut : Limit) = 1 :=580 Unitary.mul_star_self_of_mem ut.property581 rw [mul_assoc a (ut : Limit) (star (ut : Limit)), huunit, mul_one]582 constructor583 · rw [hconj]584 have hstar : star (ut : Limit) = ((star ut : unitary Limit) : Limit) := rfl585 rw [hstar, CStarRing.norm_mul_coe_unitary]586 exact hcommA587 · have hconjInv :588 star (ut : Limit) * a * (ut : Limit) - a =589 star (ut : Limit) * (a * (ut : Limit) - (ut : Limit) * a) := by590 have huunit : star (ut : Limit) * (ut : Limit) = 1 :=591 Unitary.star_mul_self_of_mem ut.property592 symm593 calc594 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 := by599 rw [mul_assoc, mul_assoc]600 _ = star (ut : Limit) * a * (ut : Limit) - a := by601 rw [huunit, one_mul]602 rw [hconjInv]603 have hstar : star (ut : Limit) = ((star ut : unitary Limit) : Limit) := rfl604 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 hcommA608609set_option maxHeartbeats 800000 in610/-- Endpoint compatibility form of finite-set exact local transport. -/611theorem exists_stageTests_exact_unitary_apply_eq_and_conjugate_sub_norm_lt612 {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 := by625 obtain ⟨n, delta, hdelta, hmain⟩ :=626 exists_stageTests_exact_unitary_path_apply_eq_and_conjugate_sub_norm_lt627 rho hrho F hepsilon628 refine ⟨n, delta, hdelta, ?_⟩629 intro xi eta hxi heta hstate630 obtain ⟨u, huapply, p, hp⟩ := hmain xi eta hxi heta hstate631 refine ⟨u, huapply, ?_⟩632 intro a ha633 have h := hp (1 : Set.Icc (0 : ℝ) 1) a ha634 simpa only [p.target] using h635636end MathlibAnnex.CStarAlgebra.CAR