OAI/Analysis/KadisonSimilarity/Representation/RestrictedNormality.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The canonical GNS model of a bounded L²-generated algebra is normal. The proof uses the actual inclusion of its trace vectors in the ambient GNS space.

  1. theorem OAI.KadisonSimilarity.restricted_generated_trace_balls_closed line 18
  2. theorem OAI.KadisonSimilarity.restricted_generated_normal_range line 49
  3. theorem OAI.KadisonSimilarity.canonicalGenerated_normal_range line 61