OAI/Analysis/KadisonSimilarity/Tracial/TracialBoundedBalls.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Closed trace-vector balls persist in the bounded L²-generated algebra. This proves normality on its own cyclic Hilbert space, not only on the ambient representation space.

  1. theorem OAI.KadisonSimilarity.TracialCornerGeometry.trace_balls_closed_of_normal_range line 18
  2. theorem OAI.KadisonSimilarity.TracialCornerGeometry.l2Generated_trace_balls_closed line 44
  3. theorem OAI.KadisonSimilarity.TracialCornerGeometry.l2Generated_normal_baseRange line 66