OAI/Analysis/KadisonKastler/SelfAdjointApproximation.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Self-adjoint approximation by the algebra and its commutant

  1. def OAI.KadisonKastler.algebraCommutantSum line 13
  2. def OAI.KadisonKastler.selfAdjointAlgebraCommutantSum line 16
  3. theorem OAI.KadisonKastler.selfAdjointAlgebraCommutantSum_subset line 20
  4. theorem OAI.KadisonKastler.selfAdjointAlgebraCommutantSum_zero line 25
  5. theorem OAI.KadisonKastler.selfAdjointAlgebraCommutantSum_add line 30
  6. theorem OAI.KadisonKastler.selfAdjointAlgebraCommutantSum_smul line 39
  7. theorem OAI.KadisonKastler.realPart_mem_vonNeumann line 50
  8. theorem OAI.KadisonKastler.exists_selfAdjoint_sum_approximation line 55
  9. theorem OAI.KadisonKastler.selfAdjoint_of_mem_algebraCommutantSum line 71
  10. theorem OAI.KadisonKastler.commutator_mem_of_mem_algebraCommutantSum line 76