OAI/Analysis/KadisonSimilarity/Tracial/TracialUltrapowerCorners.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KadisonSimilarity.tracialUltrapower_corner_bound_of_projection_lift line 20

   Source documentation

   An actual lifted projection transfers every coordinate corner bound. No action of a null algebra sequence on the whole Hilbert ultrapower is asserted.

   theorem tracialUltrapower_corner_bound_of_projection_lift
       (T : τ.GNS →L[ℂ] τ.GNS) (p : ℕ →ᵇ A) (hp : ∀ i, IsStarProjection (p i))
       (e : Ultrapower τ h1 ω htr) (he : IsStarProjection e)
       (hpe : quotientHom τ h1 ω htr p = e)
       {ε : ℝ} (hε : 0 ≤ ε)
       (hcorner : ∀ i, ∀ z : CStarCorner (p i) (hp i),
         ‖commutator T (τ.gnsStarAlgHom (z : A))‖ ≤ ε * ‖z‖)
       (z : CStarCorner e he) :
       ‖commutator (tracialUltrapowerCompression τ h1 ω htr T)
         ((quotientTrace τ h1 ω htr).gnsStarAlgHom (z : Ultrapower τ h1 ω htr))‖ ≤ ε * ‖z‖ := by
   …

   Mentions: OAI.KadisonSimilarity.CStarCorner, OAI.KadisonSimilarity.commutator, OAI.KadisonSimilarity.tracialUltrapowerCompression