OAI/Analysis/Commutator/NormalRelativeCommutant.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Kadison.NormalRelativeCommutant.liftedUnitary line 25
  2. def OAI.Kadison.NormalRelativeCommutant.orbit line 27
  3. lemma OAI.Kadison.NormalRelativeCommutant.orbit_self line 30
  4. lemma OAI.Kadison.NormalRelativeCommutant.conjugation_orbit line 34
  5. lemma OAI.Kadison.NormalRelativeCommutant.vector_injective line 41
  6. lemma OAI.Kadison.NormalRelativeCommutant.vector_unitball_convex line 49
  7. lemma OAI.Kadison.NormalRelativeCommutant.hull_bounded line 55
  8. lemma OAI.Kadison.NormalRelativeCommutant.hull_trace line 67
  9. lemma OAI.Kadison.NormalRelativeCommutant.commutes_of_fixed line 78
  10. theorem OAI.Kadison.NormalRelativeCommutant.scalar_mem_hull_contraction line 98
  11. theorem OAI.Kadison.NormalRelativeCommutant.scalar_distance_le line 122
  12. theorem OAI.Kadison.NormalRelativeCommutant.exists_unitary_witness line 140