OAI/Analysis/Pureness/Comparison/SpectralMeasure.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CuntzComparison.TracialState.spectralFunctional line 10
2. def OAI.CuntzComparison.TracialState.spectralMeasureOn line 34
3. instance OAI.CuntzComparison.(instance at line 38) line 38
4. instance OAI.CuntzComparison.(instance at line 43) line 43
5. def OAI.CuntzComparison.TracialState.spectralMeasure line 48
6. instance OAI.CuntzComparison.(instance at line 52) line 52
7. instance OAI.CuntzComparison.(instance at line 57) line 57
8. theorem OAI.CuntzComparison.TracialState.integral_spectralMeasure line 62
9. theorem OAI.CuntzComparison.TracialState.linking_spectralMeasure line 74
10. def OAI.CuntzComparison.TracialState.spectralSupportMass line 83
11. theorem OAI.CuntzComparison.TracialState.linking_support_mass line 87