OAI/Analysis/KadisonKastler/TypeIIIPartialUnitaryExtension.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Completing a proper partial isometry inside a type III factor

Nonzero complementary projections are equivalent. The completion agrees exactly on the source projection, so its vector error is controlled by the discarded source corner. This is the bounded step used to pass from isometries to unitaries in state-orbit approximation.

  1. theorem OAI.KadisonKastler.TypeIIIFactor.extend_partialIsometry line 21
  2. theorem OAI.KadisonKastler.unitary_isometry_error_of_agree line 63

    Source documentation

    Exact agreement on a projection controls the error on every vector.

    theorem unitary_isometry_error_of_agree (v : Algebra M) (hv : star v*v=1)
    (u : unitary (Algebra M)) (p : AlgebraProjection M)
    (hp : u.val*p.val=v*p.val) (ξ : H) :
    ‖u.val.val ξ-v.val ξ‖ ≤ 2*‖ξ-p.val.val ξ‖ := by
…

    Mentions: OAI.KadisonKastler.Algebra