OAI/Analysis/KadisonKastler/TraceRepresentationNormal.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Bounded weak normality of the constructed trace representation

  1. theorem OAI.KadisonKastler.boundedWeakNormal_of_ball_continuous line 21
  2. theorem OAI.KadisonKastler.traceFreeHilbertAction_boundedWeakNormal line 54
  3. theorem OAI.KadisonKastler.traceFreeHilbertEquiv_boundedWeakNormal line 62