OAI/Analysis/KadisonKastler/FreeDiagonalGNS.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

The faithful tracial Hilbert space of the generated diagonal algebra

  1. theorem OAI.KadisonKastler.inner_traceStateVector line 18
  2. def OAI.KadisonKastler.traceStateVectorContinuous line 24
  3. theorem OAI.KadisonKastler.generatedDiagonal_generatedProjection_eq_top line 35
  4. def OAI.KadisonKastler.generatedDiagonalTrace line 56
  5. theorem OAI.KadisonKastler.generatedDiagonalTrace_apply line 59
  6. theorem OAI.KadisonKastler.generatedDiagonalProjection_isProjection line 62
  7. theorem OAI.KadisonKastler.generatedDiagonalProjection_orthogonal line 71
  8. theorem OAI.KadisonKastler.generatedDiagonalProjection_sum line 78
  9. theorem OAI.KadisonKastler.generatedDiagonalLinearCombination_coe line 85
  10. theorem OAI.KadisonKastler.generatedDiagonal_scalarFree line 92
  11. theorem OAI.KadisonKastler.generatedDiagonalCentered_coe line 104
  12. theorem OAI.KadisonKastler.generatedDiagonalWord_coe line 107
  13. theorem OAI.KadisonKastler.generatedDiagonal_trace_reduced_word line 118