OAI/Analysis/KadisonKastler/ReducingFactorEquiv.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Faithful normal restriction of a factor to a nonzero reducing subspace

  1. def OAI.KadisonKastler.reducingFactorEquiv line 23
  2. theorem OAI.KadisonKastler.reducingFactorEquiv_apply line 29
  3. theorem OAI.KadisonKastler.reducingFactorEquiv_tendsto_weak line 32
  4. theorem OAI.KadisonKastler.reducingRepresentation_comparison line 43
  5. theorem OAI.KadisonKastler.scalarCenter_of_isII1 line 52