Exact source: MathlibAnnex/Analysis/CStarAlgebra/CAR/CornerLift.lean, lines 262–268.
Back to Lifting a corner involution to an ambient CAR unitary
1import MathlibAnnex.Analysis.CStarAlgebra.InvariantExponential 2import MathlibAnnex.Analysis.CStarAlgebra.CAR.FiniteAverage 3import Mathlib.Analysis.CStarAlgebra.Exponential 4import Mathlib.Analysis.CStarAlgebra.Unitary.Connected 5 6/-! 7# Unitary lift from a finite CAR corner 8 9This is the algebraic finite-corner part of the local transport construction. 10It is stated inside the completed CAR algebra and uses the actual stage matrix 11units. No representation or homogeneity statement is assumed. 12-/ 13 14set_option autoImplicit false 15 16open MathlibAnnex.Analysis.CStarAlgebra 17open MathlibAnnex.Analysis.InnerProductSpace 18open scoped Real 19 20namespace MathlibAnnex.CStarAlgebra.CAR 21 22/-- 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 0 25 star z * z = e ∧ z * star z = e ∧ e * z = z ∧ z * e = z 26 27theorem isStarProjection_limitMatrixUnit_zero_zero (n : ℕ) : 28 IsStarProjection (limitMatrixUnit n 0 0) := by 29 constructor 30 · rw [isIdempotentElem_iff] 31 simp 32 · rw [isSelfAdjoint_iff] 33 simp 34 35/-- 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 i 39 40theorem cornerLift_eq_rowAverageLinear (n : ℕ) (z : Limit) : 41 cornerLift n z = rowAverageLinear n z := rfl 42 43@[simp] 44theorem cornerLift_zero (n : ℕ) : cornerLift n 0 = 0 := by 45 simp [cornerLift] 46 47theorem star_cornerLift (n : ℕ) (z : Limit) : 48 star (cornerLift n z) = cornerLift n (star z) := by 49 classical 50 simp only [cornerLift, star_sum, star_mul, star_limitMatrixUnit] 51 apply Finset.sum_congr rfl 52 intro i _ 53 noncomm_ring 54 55private 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 := by 60 classical 61 by_cases hij : i = j 62 · subst j 63 rw [if_pos rfl] 64 calc 65 (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_ring 70 _ = limitMatrixUnit n i 0 * z * limitMatrixUnit n 0 0 * 71 star z * limitMatrixUnit n 0 i := by simp 72 _ = limitMatrixUnit n i 0 * (z * limitMatrixUnit n 0 0) * 73 star z * limitMatrixUnit n 0 i := by noncomm_ring 74 _ = limitMatrixUnit n i 0 * (z * star z) * 75 limitMatrixUnit n 0 i := by rw [hz.2.2.2]; noncomm_ring 76 _ = limitMatrixUnit n i 0 * limitMatrixUnit n 0 0 * 77 limitMatrixUnit n 0 i := by rw [hz.2.1] 78 _ = limitMatrixUnit n i i := by simp 79 · rw [if_neg hij] 80 calc 81 (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_ring 86 _ = 0 := by rw [limitMatrixUnit_mul]; simp [hij] 87 88private 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 := by 93 classical 94 by_cases hij : i = j 95 · subst j 96 rw [if_pos rfl] 97 calc 98 (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_ring 103 _ = limitMatrixUnit n i 0 * star z * limitMatrixUnit n 0 0 * 104 z * limitMatrixUnit n 0 i := by simp 105 _ = limitMatrixUnit n i 0 * star z * 106 (limitMatrixUnit n 0 0 * z) * limitMatrixUnit n 0 i := by 107 noncomm_ring 108 _ = limitMatrixUnit n i 0 * (star z * z) * 109 limitMatrixUnit n 0 i := by rw [hz.2.2.1]; noncomm_ring 110 _ = limitMatrixUnit n i 0 * limitMatrixUnit n 0 0 * 111 limitMatrixUnit n 0 i := by rw [hz.1] 112 _ = limitMatrixUnit n i i := by simp 113 · rw [if_neg hij] 114 calc 115 (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_ring 120 _ = 0 := by rw [limitMatrixUnit_mul]; simp [hij] 121 122set_option maxHeartbeats 800000 in 123/-- 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 := by 126 classical 127 rw [Unitary.mem_iff, star_cornerLift] 128 constructor 129 · simp only [cornerLift, Finset.sum_mul, Finset.mul_sum] 130 calc 131 ∑ 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 := by 135 apply Finset.sum_congr rfl 136 intro i _ 137 apply Finset.sum_congr rfl 138 intro j _ 139 exact cornerLift_star_mul_term n z hz j i 140 _ = 1 := by simp [sum_limitMatrixUnit_diag] 141 · simp only [cornerLift, Finset.sum_mul, Finset.mul_sum] 142 calc 143 ∑ 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 := by 147 apply Finset.sum_congr rfl 148 intro i _ 149 apply Finset.sum_congr rfl 150 intro j _ 151 exact cornerLift_mul_term n z hz j i 152 _ = 1 := by simp [sum_limitMatrixUnit_diag] 153 154private 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 := by 158 classical 159 simp only [cornerLift, Finset.sum_mul] 160 rw [Finset.sum_eq_single p] 161 · calc 162 (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) := by 166 noncomm_ring 167 _ = _ := by simp 168 · intro i _ hip 169 calc 170 (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) := by 174 noncomm_ring 175 _ = 0 := by rw [limitMatrixUnit_mul]; simp [hip] 176 · simp 177 178private 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 := by 182 classical 183 simp only [cornerLift, Finset.mul_sum] 184 rw [Finset.sum_eq_single q] 185 · calc 186 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_ring 190 _ = _ := by simp 191 · intro i _ hiq 192 calc 193 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_ring 197 _ = 0 := by rw [limitMatrixUnit_mul]; simp [Ne.symm hiq] 198 · simp 199 200/-- The amplified corner unitary commutes exactly with every matrix unit in 201the 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) := by 205 rw [Commute, SemiconjBy, 206 cornerLift_mul_matrixUnit n z p q, 207 matrixUnit_mul_cornerLift n z p q] 208 209/-- The lift centralizes the whole chosen finite matrix stage, not merely its 210displayed matrix units. -/ 211theorem ofStage_commute_cornerLift (n : ℕ) (c : Stage n) (z : Limit) : 212 Commute (ofStage n c) (cornerLift n z) := by 213 rw [cornerLift_eq_rowAverageLinear] 214 exact ofStage_commute_rowAverage n c z 215 216/-- The exponential of a supported self-adjoint corner element, with the 217corner projection inserted as the corner unit. -/ 218noncomputable def cornerExponential (n : ℕ) (h : selfAdjoint Limit) : Limit := 219 limitMatrixUnit n 0 0 * (selfAdjoint.expUnitary h : Limit) 220 221/-- A supported self-adjoint element exponentiates to a genuine unitary in 222the 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) := by 228 let e : Limit := limitMatrixUnit n 0 0 229 let u : Limit := selfAdjoint.expUnitary h 230 have heidem : e * e = e := by simp [e] 231 have hestar : star e = e := by simp [e] 232 have heu : Commute e u := by 233 have hehcomm : Commute e (h : Limit) := by 234 rw [Commute, SemiconjBy] 235 exact heh.trans hhe.symm 236 dsimp [u] 237 exact (hehcomm.smul_right Complex.I).exp_right 238 have hu : u ∈ unitary Limit := (selfAdjoint.expUnitary h).property 239 change star (e * u) * (e * u) = e ∧ 240 (e * u) * star (e * u) = e ∧ e * (e * u) = e * u ∧ 241 (e * u) * e = e * u 242 constructor 243 · calc 244 star (e * u) * (e * u) = star u * e * (e * u) := by rw [star_mul, hestar] 245 _ = star u * ((e * e) * u) := by noncomm_ring 246 _ = 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 constructor 251 · calc 252 (e * u) * star (e * u) = e * u * (star u * e) := by rw [star_mul, hestar] 253 _ = e * (u * star u) * e := by noncomm_ring 254 _ = e := by rw [hu.2, mul_one, heidem] 255 constructor 256 · rw [← mul_assoc, heidem] 257 · calc 258 (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] 261 262/-- 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)⟩ 269 270/-- 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) where 276 toFun t := liftedCornerExponential n ((t : ℝ) • h) 277 (by 278 change limitMatrixUnit n 0 0 * ((t : ℝ) • (h : Limit)) = 279 (t : ℝ) • (h : Limit) 280 rw [mul_smul_comm, heh]) 281 (by 282 change ((t : ℝ) • (h : Limit)) * limitMatrixUnit n 0 0 = 283 (t : ℝ) • (h : Limit) 284 rw [smul_mul_assoc, hhe]) 285 continuous_toFun := by 286 apply continuous_induced_rng.mpr 287 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) := by 291 apply continuous_induced_rng.mpr 292 change Continuous (fun t : Set.Icc (0 : ℝ) 1 => 293 ((t : ℝ) : ℂ) • (h : Limit)) 294 fun_prop 295 have hexp : Continuous (fun t : Set.Icc (0 : ℝ) 1 => 296 (selfAdjoint.expUnitary ((t : ℝ) • h) : Limit)) := 297 continuous_subtype_val.comp 298 (selfAdjoint.continuous_expUnitary.comp hsmul) 299 exact (rowAverage n).continuous.comp (continuous_const.mul hexp) 300 source' := by 301 apply Subtype.ext 302 simp [liftedCornerExponential, cornerExponential, cornerLift, 303 sum_limitMatrixUnit_diag] 304 target' := by 305 apply Subtype.ext 306 have hone : ((1 : ℝ) • h : selfAdjoint Limit) = h := by 307 apply Subtype.ext 308 change ((1 : ℝ) : ℂ) • (h : Limit) = (h : Limit) 309 simp 310 change cornerLift n (cornerExponential n ((1 : ℝ) • h)) = 311 cornerLift n (cornerExponential n h) 312 rw [hone] 313 314/-- Representation formula for the lifted corner action. -/ 315theorem representation_cornerLift_apply 316 {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) ξ)) := by 322 simp [cornerLift, map_sum, map_mul] 323 324/-- 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) 330 331/-- The lifted exponential centralizes the source stage at every time along 332its 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) := by 339 exact liftedCornerExponential_commute_stage n ((t : ℝ) • h) 340 (by 341 change limitMatrixUnit n 0 0 * ((t : ℝ) • (h : Limit)) = 342 (t : ℝ) • (h : Limit) 343 rw [mul_smul_comm, heh]) 344 (by 345 change ((t : ℝ) • (h : Limit)) * limitMatrixUnit n 0 0 = 346 (t : ℝ) • (h : Limit) 347 rw [smul_mul_assoc, hhe]) c 348 349/-- 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 1 357 (liftedCornerExponential n h₂ heh₂ hh₂e * 358 liftedCornerExponential n h₁ heh₁ hh₁e) where 359 toFun t := liftedCornerExponentialPath n h₂ heh₂ hh₂e t * 360 liftedCornerExponentialPath n h₁ heh₁ hh₁e t 361 continuous_toFun := by fun_prop 362 source' := by simp 363 target' := by 364 exact congrArg₂ (· * ·) 365 (liftedCornerExponentialPath n h₂ heh₂ hh₂e).target 366 (liftedCornerExponentialPath n h₁ heh₁ hh₁e).target 367 368/-- Both factors of the paired path centralize the source stage at every 369time, 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_right 380 (liftedCornerExponentialPath_commute_stage n h₁ heh₁ hh₁e t c) 381 382/-- CAR specialization of the supported quantitative Kadison theorem. The 383witness is already a self-adjoint element of the actual finite-stage root 384corner, ready for corner exponentiation and amplification. -/ 385theorem exists_rootCornerSupported_selfAdjoint_norm_le_one_apply_sub_norm_lt 386 {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 ξ)‖ < ε := by 400 obtain ⟨a, ha, hanorm, haleft, haright, happ⟩ := 401 ρ.exists_cornerSupported_selfAdjoint_norm_le_one_atomic_apply_sub_norm_lt 402 hρ (isStarProjection_limitMatrixUnit_zero_zero n) ξ hξ T hT hTnorm 403 hTrange hε 404 exact ⟨⟨a, ha⟩, hanorm, haleft, haright, happ⟩ 405 406/-- Exact, coarse-norm CAR corner interpolation on a finite-dimensional active 407subspace. This is the exact counterpart of the one-shot approximation above. -/ 408theorem exists_rootCornerSupported_selfAdjoint_norm_le_two_mul_and_eq_on 409 {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 := by 421 obtain ⟨a, ha, hanorm, haleft, haright, hexact⟩ := 422 rho.exists_cornerSupported_selfAdjoint_norm_le_two_mul_and_eq_on 423 hrho (isStarProjection_limitMatrixUnit_zero_zero n) E hE T hT hTrange 424 exact ⟨⟨a, ha⟩, hanorm, haleft, haright, hexact⟩ 425 426/-- A finite-dimensional invariant self-adjoint operator can be lifted into the 427root CAR corner so that the corresponding corner exponential has exactly the 428prescribed exponential action on the active subspace. -/ 429theorem exists_rootCornerSupported_exponential_eq_on 430 {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 := by 445 obtain ⟨h, hnorm, heh, hhe, hexact⟩ := 446 exists_rootCornerSupported_selfAdjoint_norm_le_two_mul_and_eq_on 447 rho hrho n E hE T hT hTrange 448 refine ⟨h, hnorm, heh, hhe, fun x hx => ?_⟩ 449 have hehcomm : Commute (limitMatrixUnit n 0 0) (h : Limit) := by 450 rw [Commute, SemiconjBy] 451 exact heh.trans hhe.symm 452 have heexp : Commute (limitMatrixUnit n 0 0) 453 (selfAdjoint.expUnitary h : Limit) := by 454 simpa only [selfAdjoint.expUnitary_coe] using 455 (hehcomm.smul_right Complex.I).exp_right 456 calc 457 rho (cornerExponential n h) x = 458 rho (limitMatrixUnit n 0 0) 459 (rho (selfAdjoint.expUnitary h : Limit) x) := by 460 simp [cornerExponential, map_mul] 461 _ = rho (selfAdjoint.expUnitary h : Limit) 462 (rho (limitMatrixUnit n 0 0) x) := by 463 exact congrArg (fun S : H →L[ℂ] H => S x) (heexp.map rho).eq 464 _ = 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 hx 467 468end MathlibAnnex.CStarAlgebra.CAR