OAI/Analysis/KadisonKastler/FactorizationCyclicSpace.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The reducing subspace generated by the left operator in a factorization. It retains every coefficient of the factored map and removes undetectable vectors from the auxiliary representation.

  1. def OAI.KadisonKastler.factorizationCyclicSpace line 19
  2. theorem OAI.KadisonKastler.mem_factorizationCyclicSpace line 23
  3. theorem OAI.KadisonKastler.left_mem_factorizationCyclicSpace line 28
  4. theorem OAI.KadisonKastler.factorizationCyclicSpace_invariant line 32
  5. instance OAI.KadisonKastler.factorizationCyclicSpace_complete line 45
  6. def OAI.KadisonKastler.cyclicFactorRepresentation line 49
  7. theorem OAI.KadisonKastler.cyclicFactorRepresentation_apply line 85
  8. def OAI.KadisonKastler.cyclicFactorLeft line 90
  9. theorem OAI.KadisonKastler.cyclicFactorLeft_apply line 94
  10. theorem OAI.KadisonKastler.factorizationCyclicSpace_total line 98