OAI/Analysis/Commutator/TracialRelativeCommutant.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Kadison.TracialSequence.unitarySequence line 23
  2. lemma OAI.Kadison.TracialSequence.unitarySequence_apply line 30
  3. lemma OAI.Kadison.TracialSequence.unitarySequence_star_mul line 33
  4. lemma OAI.Kadison.TracialSequence.unitarySequence_mul_star line 38
  5. lemma OAI.Kadison.TracialSequence.conjugate_difference_map_zero line 43
  6. lemma OAI.Kadison.TracialSequence.algHom_eq_smul_one_of_sub line 48
  7. lemma OAI.Kadison.TracialSequence.norm_map_sub_smul_le line 52
  8. theorem OAI.Kadison.TracialSequence.commutant_contraction_sequence line 65
  9. lemma OAI.Kadison.TracialSequence.algHom_commutes_smul line 115
  10. lemma OAI.Kadison.TracialSequence.algHom_scalar_of_smul line 120
  11. lemma OAI.Kadison.TracialSequence.scalar_of_contractions line 127
  12. lemma OAI.Kadison.TracialSequence.scalar_of_range line 142
  13. theorem OAI.Kadison.TracialSequence.commutant_sequence_scalar line 150
  14. theorem OAI.Kadison.TracialSequence.full_relative_commutant_scalar line 165