OAI/Analysis/KadisonSimilarity/Tracial/NormalTracialExpectations.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Trace-preserving expectations on the actual normal subalgebras of a faithful tracial geometry, including its constructed L²-generated algebras.

  1. theorem OAI.KadisonSimilarity.TracialCornerGeometry.tracialExpectation_of_normal_range line 17
  2. theorem OAI.KadisonSimilarity.TracialCornerGeometry.l2Generated_tracialExpectation line 47