OAI/Analysis/BoundedHochschild/Dixmier.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Hilbert-space averaging and central elements in unitary orbit closures.

  1. def OAI.HochschildDixmier.gnsVector line 35
  2. lemma OAI.HochschildDixmier.gnsVector_norm line 38
  3. theorem OAI.HochschildDixmier.isClosed_gns_ball line 44
  4. def OAI.HochschildDixmier.conjugate line 64
  5. lemma OAI.HochschildDixmier.conjugate_apply line 70
  6. lemma OAI.HochschildDixmier.conjugate_norm line 74
  7. lemma OAI.HochschildDixmier.conjugate_mul line 79
  8. lemma OAI.HochschildDixmier.conjugate_gns_norm line 82
  9. lemma OAI.HochschildDixmier.conjugate_hull line 97
  10. lemma OAI.HochschildDixmier.orbit_hull_bounded line 106
  11. theorem OAI.HochschildDixmier.orbit_closure_lift line 116
  12. lemma OAI.HochschildDixmier.conjugate_mem_orbit_closure line 127
  13. lemma OAI.HochschildDixmier.orbit_gns_convex line 144
  14. lemma OAI.HochschildDixmier.exists_min_norm line 152
  15. lemma OAI.HochschildDixmier.min_norm_unique line 162
  16. theorem OAI.HochschildDixmier.exists_central_average line 179
  17. lemma OAI.HochschildDixmier.trace_conjugate line 218
  18. lemma OAI.HochschildDixmier.trace_orbit_hull line 223
  19. lemma OAI.HochschildDixmier.trace_orbit_closure line 231
  20. theorem OAI.HochschildDixmier.scalar_mem_orbit_closure line 249