Exact source: MathlibAnnex/Analysis/CStarAlgebra/CAR/CornerLift.lean
Pinned GitHub source · Raw UTF-8 source
Back to Lifting a corner involution to an ambient CAR unitary
1import MathlibAnnex.Analysis.CStarAlgebra.InvariantExponential2import MathlibAnnex.Analysis.CStarAlgebra.CAR.FiniteAverage3import Mathlib.Analysis.CStarAlgebra.Exponential4import Mathlib.Analysis.CStarAlgebra.Unitary.Connected56/-!7# Unitary lift from a finite CAR corner89This is the algebraic finite-corner part of the local transport construction.10It is stated inside the completed CAR algebra and uses the actual stage matrix11units. No representation or homogeneity statement is assumed.12-/1314set_option autoImplicit false1516open MathlibAnnex.Analysis.CStarAlgebra17open MathlibAnnex.Analysis.InnerProductSpace18open scoped Real1920namespace MathlibAnnex.CStarAlgebra.CAR2122/-- A unitary in the `e₀₀` corner, with the corner projection as its unit. -/23def IsRootCornerUnitary (n : ℕ) (z : Limit) : Prop :=24 let e := limitMatrixUnit n 0 025 star z * z = e ∧ z * star z = e ∧ e * z = z ∧ z * e = z2627theorem isStarProjection_limitMatrixUnit_zero_zero (n : ℕ) :28 IsStarProjection (limitMatrixUnit n 0 0) := by29 constructor30 · rw [isIdempotentElem_iff]31 simp32 · rw [isSelfAdjoint_iff]33 simp3435/-- Matrix amplification of an element in the root corner. -/36noncomputable def cornerLift (n : ℕ) (z : Limit) : Limit :=37 ∑ i : Fin (2 ^ n),38 limitMatrixUnit n i 0 * z * limitMatrixUnit n 0 i3940theorem cornerLift_eq_rowAverageLinear (n : ℕ) (z : Limit) :41 cornerLift n z = rowAverageLinear n z := rfl4243@[simp]44theorem cornerLift_zero (n : ℕ) : cornerLift n 0 = 0 := by45 simp [cornerLift]4647theorem star_cornerLift (n : ℕ) (z : Limit) :48 star (cornerLift n z) = cornerLift n (star z) := by49 classical50 simp only [cornerLift, star_sum, star_mul, star_limitMatrixUnit]51 apply Finset.sum_congr rfl52 intro i _53 noncomm_ring5455private theorem cornerLift_mul_term (n : ℕ) (z : Limit)56 (hz : IsRootCornerUnitary n z) (i j : Fin (2 ^ n)) :57 (limitMatrixUnit n i 0 * z * limitMatrixUnit n 0 i) *58 (limitMatrixUnit n j 0 * star z * limitMatrixUnit n 0 j) =59 if i = j then limitMatrixUnit n i i else 0 := by60 classical61 by_cases hij : i = j62 · subst j63 rw [if_pos rfl]64 calc65 (limitMatrixUnit n i 0 * z * limitMatrixUnit n 0 i) *66 (limitMatrixUnit n i 0 * star z * limitMatrixUnit n 0 i) =67 limitMatrixUnit n i 0 * z *68 (limitMatrixUnit n 0 i * limitMatrixUnit n i 0) *69 star z * limitMatrixUnit n 0 i := by noncomm_ring70 _ = limitMatrixUnit n i 0 * z * limitMatrixUnit n 0 0 *71 star z * limitMatrixUnit n 0 i := by simp72 _ = limitMatrixUnit n i 0 * (z * limitMatrixUnit n 0 0) *73 star z * limitMatrixUnit n 0 i := by noncomm_ring74 _ = limitMatrixUnit n i 0 * (z * star z) *75 limitMatrixUnit n 0 i := by rw [hz.2.2.2]; noncomm_ring76 _ = limitMatrixUnit n i 0 * limitMatrixUnit n 0 0 *77 limitMatrixUnit n 0 i := by rw [hz.2.1]78 _ = limitMatrixUnit n i i := by simp79 · rw [if_neg hij]80 calc81 (limitMatrixUnit n i 0 * z * limitMatrixUnit n 0 i) *82 (limitMatrixUnit n j 0 * star z * limitMatrixUnit n 0 j) =83 limitMatrixUnit n i 0 * z *84 (limitMatrixUnit n 0 i * limitMatrixUnit n j 0) *85 star z * limitMatrixUnit n 0 j := by noncomm_ring86 _ = 0 := by rw [limitMatrixUnit_mul]; simp [hij]8788private theorem cornerLift_star_mul_term (n : ℕ) (z : Limit)89 (hz : IsRootCornerUnitary n z) (i j : Fin (2 ^ n)) :90 (limitMatrixUnit n i 0 * star z * limitMatrixUnit n 0 i) *91 (limitMatrixUnit n j 0 * z * limitMatrixUnit n 0 j) =92 if i = j then limitMatrixUnit n i i else 0 := by93 classical94 by_cases hij : i = j95 · subst j96 rw [if_pos rfl]97 calc98 (limitMatrixUnit n i 0 * star z * limitMatrixUnit n 0 i) *99 (limitMatrixUnit n i 0 * z * limitMatrixUnit n 0 i) =100 limitMatrixUnit n i 0 * star z *101 (limitMatrixUnit n 0 i * limitMatrixUnit n i 0) *102 z * limitMatrixUnit n 0 i := by noncomm_ring103 _ = limitMatrixUnit n i 0 * star z * limitMatrixUnit n 0 0 *104 z * limitMatrixUnit n 0 i := by simp105 _ = limitMatrixUnit n i 0 * star z *106 (limitMatrixUnit n 0 0 * z) * limitMatrixUnit n 0 i := by107 noncomm_ring108 _ = limitMatrixUnit n i 0 * (star z * z) *109 limitMatrixUnit n 0 i := by rw [hz.2.2.1]; noncomm_ring110 _ = limitMatrixUnit n i 0 * limitMatrixUnit n 0 0 *111 limitMatrixUnit n 0 i := by rw [hz.1]112 _ = limitMatrixUnit n i i := by simp113 · rw [if_neg hij]114 calc115 (limitMatrixUnit n i 0 * star z * limitMatrixUnit n 0 i) *116 (limitMatrixUnit n j 0 * z * limitMatrixUnit n 0 j) =117 limitMatrixUnit n i 0 * star z *118 (limitMatrixUnit n 0 i * limitMatrixUnit n j 0) *119 z * limitMatrixUnit n 0 j := by noncomm_ring120 _ = 0 := by rw [limitMatrixUnit_mul]; simp [hij]121122set_option maxHeartbeats 800000 in123/-- A corner unitary amplifies to a unitary of the completed CAR algebra. -/124theorem cornerLift_mem_unitary (n : ℕ) (z : Limit)125 (hz : IsRootCornerUnitary n z) : cornerLift n z ∈ unitary Limit := by126 classical127 rw [Unitary.mem_iff, star_cornerLift]128 constructor129 · simp only [cornerLift, Finset.sum_mul, Finset.mul_sum]130 calc131 ∑ j, ∑ i,132 (limitMatrixUnit n i 0 * star z * limitMatrixUnit n 0 i) *133 (limitMatrixUnit n j 0 * z * limitMatrixUnit n 0 j) =134 ∑ j, ∑ i, if i = j then limitMatrixUnit n i i else 0 := by135 apply Finset.sum_congr rfl136 intro i _137 apply Finset.sum_congr rfl138 intro j _139 exact cornerLift_star_mul_term n z hz j i140 _ = 1 := by simp [sum_limitMatrixUnit_diag]141 · simp only [cornerLift, Finset.sum_mul, Finset.mul_sum]142 calc143 ∑ j, ∑ i,144 (limitMatrixUnit n i 0 * z * limitMatrixUnit n 0 i) *145 (limitMatrixUnit n j 0 * star z * limitMatrixUnit n 0 j) =146 ∑ j, ∑ i, if i = j then limitMatrixUnit n i i else 0 := by147 apply Finset.sum_congr rfl148 intro i _149 apply Finset.sum_congr rfl150 intro j _151 exact cornerLift_mul_term n z hz j i152 _ = 1 := by simp [sum_limitMatrixUnit_diag]153154private theorem cornerLift_mul_matrixUnit (n : ℕ) (z : Limit)155 (p q : Fin (2 ^ n)) :156 cornerLift n z * limitMatrixUnit n p q =157 limitMatrixUnit n p 0 * z * limitMatrixUnit n 0 q := by158 classical159 simp only [cornerLift, Finset.sum_mul]160 rw [Finset.sum_eq_single p]161 · calc162 (limitMatrixUnit n p 0 * z * limitMatrixUnit n 0 p) *163 limitMatrixUnit n p q =164 limitMatrixUnit n p 0 * z *165 (limitMatrixUnit n 0 p * limitMatrixUnit n p q) := by166 noncomm_ring167 _ = _ := by simp168 · intro i _ hip169 calc170 (limitMatrixUnit n i 0 * z * limitMatrixUnit n 0 i) *171 limitMatrixUnit n p q =172 limitMatrixUnit n i 0 * z *173 (limitMatrixUnit n 0 i * limitMatrixUnit n p q) := by174 noncomm_ring175 _ = 0 := by rw [limitMatrixUnit_mul]; simp [hip]176 · simp177178private theorem matrixUnit_mul_cornerLift (n : ℕ) (z : Limit)179 (p q : Fin (2 ^ n)) :180 limitMatrixUnit n p q * cornerLift n z =181 limitMatrixUnit n p 0 * z * limitMatrixUnit n 0 q := by182 classical183 simp only [cornerLift, Finset.mul_sum]184 rw [Finset.sum_eq_single q]185 · calc186 limitMatrixUnit n p q *187 (limitMatrixUnit n q 0 * z * limitMatrixUnit n 0 q) =188 (limitMatrixUnit n p q * limitMatrixUnit n q 0) * z *189 limitMatrixUnit n 0 q := by noncomm_ring190 _ = _ := by simp191 · intro i _ hiq192 calc193 limitMatrixUnit n p q *194 (limitMatrixUnit n i 0 * z * limitMatrixUnit n 0 i) =195 (limitMatrixUnit n p q * limitMatrixUnit n i 0) * z *196 limitMatrixUnit n 0 i := by noncomm_ring197 _ = 0 := by rw [limitMatrixUnit_mul]; simp [Ne.symm hiq]198 · simp199200/-- The amplified corner unitary commutes exactly with every matrix unit in201the chosen finite stage. -/202theorem cornerLift_commute_matrixUnit (n : ℕ) (z : Limit)203 (p q : Fin (2 ^ n)) :204 Commute (cornerLift n z) (limitMatrixUnit n p q) := by205 rw [Commute, SemiconjBy,206 cornerLift_mul_matrixUnit n z p q,207 matrixUnit_mul_cornerLift n z p q]208209/-- The lift centralizes the whole chosen finite matrix stage, not merely its210displayed matrix units. -/211theorem ofStage_commute_cornerLift (n : ℕ) (c : Stage n) (z : Limit) :212 Commute (ofStage n c) (cornerLift n z) := by213 rw [cornerLift_eq_rowAverageLinear]214 exact ofStage_commute_rowAverage n c z215216/-- The exponential of a supported self-adjoint corner element, with the217corner projection inserted as the corner unit. -/218noncomputable def cornerExponential (n : ℕ) (h : selfAdjoint Limit) : Limit :=219 limitMatrixUnit n 0 0 * (selfAdjoint.expUnitary h : Limit)220221/-- A supported self-adjoint element exponentiates to a genuine unitary in222the root corner. -/223theorem isRootCornerUnitary_cornerExponential (n : ℕ)224 (h : selfAdjoint Limit)225 (heh : limitMatrixUnit n 0 0 * (h : Limit) = h)226 (hhe : (h : Limit) * limitMatrixUnit n 0 0 = h) :227 IsRootCornerUnitary n (cornerExponential n h) := by228 let e : Limit := limitMatrixUnit n 0 0229 let u : Limit := selfAdjoint.expUnitary h230 have heidem : e * e = e := by simp [e]231 have hestar : star e = e := by simp [e]232 have heu : Commute e u := by233 have hehcomm : Commute e (h : Limit) := by234 rw [Commute, SemiconjBy]235 exact heh.trans hhe.symm236 dsimp [u]237 exact (hehcomm.smul_right Complex.I).exp_right238 have hu : u ∈ unitary Limit := (selfAdjoint.expUnitary h).property239 change star (e * u) * (e * u) = e ∧240 (e * u) * star (e * u) = e ∧ e * (e * u) = e * u ∧241 (e * u) * e = e * u242 constructor243 · calc244 star (e * u) * (e * u) = star u * e * (e * u) := by rw [star_mul, hestar]245 _ = star u * ((e * e) * u) := by noncomm_ring246 _ = star u * (e * u) := by rw [heidem]247 _ = star u * (u * e) := by rw [heu.eq]248 _ = (star u * u) * e := by rw [mul_assoc]249 _ = e := by rw [hu.1, one_mul]250 constructor251 · calc252 (e * u) * star (e * u) = e * u * (star u * e) := by rw [star_mul, hestar]253 _ = e * (u * star u) * e := by noncomm_ring254 _ = e := by rw [hu.2, mul_one, heidem]255 constructor256 · rw [← mul_assoc, heidem]257 · calc258 (e * u) * e = e * (u * e) := by rw [mul_assoc]259 _ = e * (e * u) := by rw [heu.eq]260 _ = e * u := by rw [← mul_assoc, heidem]261262/-- The fully amplified corner exponential as an ambient CAR unitary. -/263noncomputable def liftedCornerExponential (n : ℕ) (h : selfAdjoint Limit)264 (heh : limitMatrixUnit n 0 0 * (h : Limit) = h)265 (hhe : (h : Limit) * limitMatrixUnit n 0 0 = h) : unitary Limit :=266 ⟨cornerLift n (cornerExponential n h),267 cornerLift_mem_unitary n (cornerExponential n h)268 (isRootCornerUnitary_cornerExponential n h heh hhe)⟩269270/-- The canonical path from the ambient unit to a lifted corner exponential.271Every intermediate generator remains supported in the same root corner. -/272noncomputable def liftedCornerExponentialPath (n : ℕ) (h : selfAdjoint Limit)273 (heh : limitMatrixUnit n 0 0 * (h : Limit) = h)274 (hhe : (h : Limit) * limitMatrixUnit n 0 0 = h) :275 Path 1 (liftedCornerExponential n h heh hhe) where276 toFun t := liftedCornerExponential n ((t : ℝ) • h)277 (by278 change limitMatrixUnit n 0 0 * ((t : ℝ) • (h : Limit)) =279 (t : ℝ) • (h : Limit)280 rw [mul_smul_comm, heh])281 (by282 change ((t : ℝ) • (h : Limit)) * limitMatrixUnit n 0 0 =283 (t : ℝ) • (h : Limit)284 rw [smul_mul_assoc, hhe])285 continuous_toFun := by286 apply continuous_induced_rng.mpr287 change Continuous (fun t : Set.Icc (0 : ℝ) 1 =>288 rowAverage n (limitMatrixUnit n 0 0 *289 (selfAdjoint.expUnitary ((t : ℝ) • h) : Limit)))290 have hsmul : Continuous (fun t : Set.Icc (0 : ℝ) 1 => (t : ℝ) • h) := by291 apply continuous_induced_rng.mpr292 change Continuous (fun t : Set.Icc (0 : ℝ) 1 =>293 ((t : ℝ) : ℂ) • (h : Limit))294 fun_prop295 have hexp : Continuous (fun t : Set.Icc (0 : ℝ) 1 =>296 (selfAdjoint.expUnitary ((t : ℝ) • h) : Limit)) :=297 continuous_subtype_val.comp298 (selfAdjoint.continuous_expUnitary.comp hsmul)299 exact (rowAverage n).continuous.comp (continuous_const.mul hexp)300 source' := by301 apply Subtype.ext302 simp [liftedCornerExponential, cornerExponential, cornerLift,303 sum_limitMatrixUnit_diag]304 target' := by305 apply Subtype.ext306 have hone : ((1 : ℝ) • h : selfAdjoint Limit) = h := by307 apply Subtype.ext308 change ((1 : ℝ) : ℂ) • (h : Limit) = (h : Limit)309 simp310 change cornerLift n (cornerExponential n ((1 : ℝ) • h)) =311 cornerLift n (cornerExponential n h)312 rw [hone]313314/-- Representation formula for the lifted corner action. -/315theorem representation_cornerLift_apply316 {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]317 (ρ : Representation Limit H) (n : ℕ) (z : Limit) (ξ : H) :318 ρ (cornerLift n z) ξ =319 ∑ i : Fin (2 ^ n),320 ρ (limitMatrixUnit n i 0)321 (ρ z (ρ (limitMatrixUnit n 0 i) ξ)) := by322 simp [cornerLift, map_sum, map_mul]323324/-- Every lifted corner exponential centralizes its source stage exactly. -/325theorem liftedCornerExponential_commute_stage (n : ℕ) (h : selfAdjoint Limit)326 (heh : limitMatrixUnit n 0 0 * (h : Limit) = h)327 (hhe : (h : Limit) * limitMatrixUnit n 0 0 = h) (c : Stage n) :328 Commute (ofStage n c) (liftedCornerExponential n h heh hhe : Limit) :=329 ofStage_commute_cornerLift n c (cornerExponential n h)330331/-- The lifted exponential centralizes the source stage at every time along332its canonical path, not only at the endpoint. -/333theorem liftedCornerExponentialPath_commute_stage (n : ℕ)334 (h : selfAdjoint Limit)335 (heh : limitMatrixUnit n 0 0 * (h : Limit) = h)336 (hhe : (h : Limit) * limitMatrixUnit n 0 0 = h)337 (t : Set.Icc (0 : ℝ) 1) (c : Stage n) :338 Commute (ofStage n c) (liftedCornerExponentialPath n h heh hhe t : Limit) := by339 exact liftedCornerExponential_commute_stage n ((t : ℝ) • h)340 (by341 change limitMatrixUnit n 0 0 * ((t : ℝ) • (h : Limit)) =342 (t : ℝ) • (h : Limit)343 rw [mul_smul_comm, heh])344 (by345 change ((t : ℝ) • (h : Limit)) * limitMatrixUnit n 0 0 =346 (t : ℝ) • (h : Limit)347 rw [smul_mul_assoc, hhe]) c348349/-- The pointwise product of two lifted corner-exponential paths. -/350noncomputable def liftedCornerExponentialPairPath (n : ℕ)351 (h₁ h₂ : selfAdjoint Limit)352 (heh₁ : limitMatrixUnit n 0 0 * (h₁ : Limit) = h₁)353 (hh₁e : (h₁ : Limit) * limitMatrixUnit n 0 0 = h₁)354 (heh₂ : limitMatrixUnit n 0 0 * (h₂ : Limit) = h₂)355 (hh₂e : (h₂ : Limit) * limitMatrixUnit n 0 0 = h₂) :356 Path 1357 (liftedCornerExponential n h₂ heh₂ hh₂e *358 liftedCornerExponential n h₁ heh₁ hh₁e) where359 toFun t := liftedCornerExponentialPath n h₂ heh₂ hh₂e t *360 liftedCornerExponentialPath n h₁ heh₁ hh₁e t361 continuous_toFun := by fun_prop362 source' := by simp363 target' := by364 exact congrArg₂ (· * ·)365 (liftedCornerExponentialPath n h₂ heh₂ hh₂e).target366 (liftedCornerExponentialPath n h₁ heh₁ hh₁e).target367368/-- Both factors of the paired path centralize the source stage at every369time, hence so does their product. -/370theorem liftedCornerExponentialPairPath_commute_stage (n : ℕ)371 (h₁ h₂ : selfAdjoint Limit)372 (heh₁ : limitMatrixUnit n 0 0 * (h₁ : Limit) = h₁)373 (hh₁e : (h₁ : Limit) * limitMatrixUnit n 0 0 = h₁)374 (heh₂ : limitMatrixUnit n 0 0 * (h₂ : Limit) = h₂)375 (hh₂e : (h₂ : Limit) * limitMatrixUnit n 0 0 = h₂)376 (t : Set.Icc (0 : ℝ) 1) (c : Stage n) :377 Commute (ofStage n c)378 (liftedCornerExponentialPairPath n h₁ h₂ heh₁ hh₁e heh₂ hh₂e t : Limit) :=379 (liftedCornerExponentialPath_commute_stage n h₂ heh₂ hh₂e t c).mul_right380 (liftedCornerExponentialPath_commute_stage n h₁ heh₁ hh₁e t c)381382/-- CAR specialization of the supported quantitative Kadison theorem. The383witness is already a self-adjoint element of the actual finite-stage root384corner, ready for corner exponentiation and amplification. -/385theorem exists_rootCornerSupported_selfAdjoint_norm_le_one_apply_sub_norm_lt386 {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H]387 [CompleteSpace H] [Nontrivial H]388 (ρ : Representation Limit H) (hρ : StarAlgHom.IsIrreducible ρ)389 (n : ℕ) {I : Type*} [Fintype I] [DecidableEq I]390 (ξ : I → H) (hξ : ∀ i, ρ (limitMatrixUnit n 0 0) (ξ i) = ξ i)391 (T : H →L[ℂ] H) (hT : IsSelfAdjoint T) (hTnorm : ‖T‖ ≤ 1)392 (hTrange : ρ (limitMatrixUnit n 0 0) * T = T)393 {ε : ℝ} (hε : 0 < ε) :394 ∃ h : selfAdjoint Limit, ‖(h : Limit)‖ ≤ 1 ∧395 limitMatrixUnit n 0 0 * (h : Limit) = h ∧396 (h : Limit) * limitMatrixUnit n 0 0 = h ∧397 ‖atomicRepresentation (fun _ : I => ρ) (h : Limit) (finiteHilbertSum ξ) -398 diagonal (fun _ : I => T) ‖T‖ (norm_nonneg T) (fun _ => le_rfl)399 (finiteHilbertSum ξ)‖ < ε := by400 obtain ⟨a, ha, hanorm, haleft, haright, happ⟩ :=401 ρ.exists_cornerSupported_selfAdjoint_norm_le_one_atomic_apply_sub_norm_lt402 hρ (isStarProjection_limitMatrixUnit_zero_zero n) ξ hξ T hT hTnorm403 hTrange hε404 exact ⟨⟨a, ha⟩, hanorm, haleft, haright, happ⟩405406/-- Exact, coarse-norm CAR corner interpolation on a finite-dimensional active407subspace. This is the exact counterpart of the one-shot approximation above. -/408theorem exists_rootCornerSupported_selfAdjoint_norm_le_two_mul_and_eq_on409 {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H]410 [CompleteSpace H] [Nontrivial H]411 (rho : Representation Limit H) (hrho : StarAlgHom.IsIrreducible rho)412 (n : ℕ) (E : Submodule ℂ H) [E.HasOrthogonalProjection]413 [FiniteDimensional ℂ E]414 (hE : ∀ x : H, x ∈ E → rho (limitMatrixUnit n 0 0) x = x)415 (T : H →L[ℂ] H) (hT : IsSelfAdjoint T)416 (hTrange : rho (limitMatrixUnit n 0 0) * T = T) :417 ∃ h : selfAdjoint Limit, ‖(h : Limit)‖ ≤ 2 * ‖T‖ ∧418 limitMatrixUnit n 0 0 * (h : Limit) = h ∧419 (h : Limit) * limitMatrixUnit n 0 0 = h ∧420 ∀ x : H, x ∈ E → rho (h : Limit) x = T x := by421 obtain ⟨a, ha, hanorm, haleft, haright, hexact⟩ :=422 rho.exists_cornerSupported_selfAdjoint_norm_le_two_mul_and_eq_on423 hrho (isStarProjection_limitMatrixUnit_zero_zero n) E hE T hT hTrange424 exact ⟨⟨a, ha⟩, hanorm, haleft, haright, hexact⟩425426/-- A finite-dimensional invariant self-adjoint operator can be lifted into the427root CAR corner so that the corresponding corner exponential has exactly the428prescribed exponential action on the active subspace. -/429theorem exists_rootCornerSupported_exponential_eq_on430 {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H]431 [CompleteSpace H] [Nontrivial H]432 (rho : Representation Limit H) (hrho : StarAlgHom.IsIrreducible rho)433 (n : ℕ) (E : Submodule ℂ H) [E.HasOrthogonalProjection]434 [FiniteDimensional ℂ E]435 (hE : ∀ x : H, x ∈ E → rho (limitMatrixUnit n 0 0) x = x)436 (T : H →L[ℂ] H) (hT : IsSelfAdjoint T)437 (hTrange : rho (limitMatrixUnit n 0 0) * T = T)438 (hTmap : Set.MapsTo T E E) :439 ∃ h : selfAdjoint Limit, ‖(h : Limit)‖ ≤ 2 * ‖T‖ ∧440 limitMatrixUnit n 0 0 * (h : Limit) = h ∧441 (h : Limit) * limitMatrixUnit n 0 0 = h ∧442 ∀ x : H, x ∈ E →443 rho (cornerExponential n h) x =444 NormedSpace.exp (Complex.I • T) x := by445 obtain ⟨h, hnorm, heh, hhe, hexact⟩ :=446 exists_rootCornerSupported_selfAdjoint_norm_le_two_mul_and_eq_on447 rho hrho n E hE T hT hTrange448 refine ⟨h, hnorm, heh, hhe, fun x hx => ?_⟩449 have hehcomm : Commute (limitMatrixUnit n 0 0) (h : Limit) := by450 rw [Commute, SemiconjBy]451 exact heh.trans hhe.symm452 have heexp : Commute (limitMatrixUnit n 0 0)453 (selfAdjoint.expUnitary h : Limit) := by454 simpa only [selfAdjoint.expUnitary_coe] using455 (hehcomm.smul_right Complex.I).exp_right456 calc457 rho (cornerExponential n h) x =458 rho (limitMatrixUnit n 0 0)459 (rho (selfAdjoint.expUnitary h : Limit) x) := by460 simp [cornerExponential, map_mul]461 _ = rho (selfAdjoint.expUnitary h : Limit)462 (rho (limitMatrixUnit n 0 0) x) := by463 exact congrArg (fun S : H →L[ℂ] H => S x) (heexp.map rho).eq464 _ = rho (selfAdjoint.expUnitary h : Limit) x := by rw [hE x hx]465 _ = NormedSpace.exp (Complex.I • T) x :=466 rho.expUnitary_apply_eq_of_eqOn_of_mapsTo h T E hexact hTmap hx467468end MathlibAnnex.CStarAlgebra.CAR