OAI/Analysis/KadisonSimilarity/Representation/CommonCommutantFields.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Every member of the original abelian commutant has an actual operator field over the common spectral measure. The construction retains its norm and its algebraic operations almost everywhere.

  1. theorem OAI.KadisonSimilarity.commutant_commutes_representation line 24
  2. def OAI.KadisonSimilarity.commonCommutantField line 31
  3. theorem OAI.KadisonSimilarity.commonCommutantField_action line 39
  4. theorem OAI.KadisonSimilarity.commonCommutantField_norm_iff line 46
  5. theorem OAI.KadisonSimilarity.commonCommutantField_add line 54
  6. theorem OAI.KadisonSimilarity.commonCommutantField_sub line 67
  7. theorem OAI.KadisonSimilarity.commonCommutantField_mul line 91
  8. theorem OAI.KadisonSimilarity.commonCommutantField_matrix_norm_iff line 104