OAI/Analysis/KadisonKastler/WeakRowAction.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Finite row averages act continuously on the compact completely bounded ball.

  1. theorem OAI.KadisonKastler.boundedWeakAlgebraCoefficients_injective line 21
  2. instance OAI.KadisonKastler.boundedWeakAlgebraMapT2 line 38
  3. def OAI.KadisonKastler.boundedWeakRowAverage line 42
  4. theorem OAI.KadisonKastler.boundedWeakRowAverage_coefficient line 47
  5. theorem OAI.KadisonKastler.continuous_boundedWeakRowAverage line 55