OAI/Analysis/KadisonKastler/TypeIIIIsometryStateOrbit.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Isometric state compressions are in the norm closure of the unitary orbit

  1. theorem OAI.KadisonKastler.TypeIIIFactor.approximate_isometry_on_vector line 17
  2. theorem OAI.KadisonKastler.TypeIIIFactor.unitary_state_close_to_isometry line 56

    Source documentation

    The final unitary replacement needed after an isometric state comparison.

    theorem TypeIIIFactor.unitary_state_close_to_isometry (hM : TypeIIIFactor M)
    (v : Algebra M) (hv : star v*v=1) (ξ : H) (hξ : ‖ξ‖=1)
    {ε : ℝ} (hε : 0 < ε) :
    ∃ u : unitary (Algebra M),
      ‖sandwichFunctional (vectorFunctional ξ) u.val-
        sandwichFunctional (vectorFunctional ξ) v‖<ε := by
…

    Mentions: OAI.KadisonKastler.TypeIIIFactor, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.sandwichFunctional