OAI/Analysis/KadisonKastler/StateScalingPartialIsometry.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Centralizer supports of state-scaling partial isometries

  1. def OAI.KadisonKastler.stateCentralizerProjection line 17
  2. def OAI.KadisonKastler.stateCentralizerInclusion line 24
  3. def OAI.KadisonKastler.includeCentralizerProjection line 28
  4. def OAI.KadisonKastler.includeCentralizerPartialIsometry line 33
  5. theorem OAI.KadisonKastler.includeCentralizerPartialIsometry_target line 43
  6. theorem OAI.KadisonKastler.partialIsometry_compose_target_of_eq line 51
  7. theorem OAI.KadisonKastler.stateScales_compose line 58
  8. theorem OAI.KadisonKastler.includeCentralizerPartialIsometry_scales line 64
  9. def OAI.KadisonKastler.scalingSupport line 69
  10. def OAI.KadisonKastler.scalingTarget line 77
  11. theorem OAI.KadisonKastler.scalingSupport_trace line 82
  12. def OAI.KadisonKastler.cutPartialIsometryTarget line 93

    Source documentation

    Restrict the final projection of a partial isometry.

    def cutPartialIsometryTarget (v : PartialIsometry M) (p : AlgebraProjection M)
    (hp : p ≤ v.target) : PartialIsometry M :=
…
  13. theorem OAI.KadisonKastler.cutPartialIsometryTarget_val line 99
  14. theorem OAI.KadisonKastler.cutPartialIsometryTarget_target line 104
  15. theorem OAI.KadisonKastler.cutPartialIsometryTarget_scales line 114