OAI/Analysis/KadisonKastler/SimultaneousRowFamily.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

A compact product keeps the same normalized rows for an entire family of completely bounded maps. Minimality descends to each coordinate.

  1. abbrev OAI.KadisonKastler.WeakMapFamily line 15
  2. def OAI.KadisonKastler.familyRowAverage line 18
  3. def OAI.KadisonKastler.familyRowOrbit line 22
  4. def OAI.KadisonKastler.FamilyRowInvariant line 26
  5. theorem OAI.KadisonKastler.continuous_familyRowAverage line 30
  6. theorem OAI.KadisonKastler.familyRowOrbit_self line 36
  7. theorem OAI.KadisonKastler.familyRowOrbit_invariant line 44
  8. theorem OAI.KadisonKastler.familyRowInvariant_closure_orbit line 62
  9. theorem OAI.KadisonKastler.exists_minimal_familyRowFamily line 69