OAI/Analysis/KadisonKastler/StateOrbitCompact.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Compact asymptotic state-central orbit hulls

The intersection of the decreasing weakly closed convex hulls contains the original operator and remains in its operator-norm ball.

  1. theorem OAI.KadisonKastler.weakOperatorBall_convex line 20
  2. theorem OAI.KadisonKastler.stateOrbitHull_subset_ball line 31
  3. theorem OAI.KadisonKastler.stateOrbitHull_compact line 44
  4. theorem OAI.KadisonKastler.stateOrbitHull_mono line 49
  5. theorem OAI.KadisonKastler.self_mem_stateOrbitHull line 56
  6. def OAI.KadisonKastler.stateOrbitCore line 66
  7. theorem OAI.KadisonKastler.self_mem_stateOrbitCore line 69
  8. theorem OAI.KadisonKastler.stateOrbitCore_closed line 73
  9. theorem OAI.KadisonKastler.stateOrbitCore_convex line 77
  10. theorem OAI.KadisonKastler.stateOrbitCore_subset_ball line 81
  11. theorem OAI.KadisonKastler.stateOrbitCore_compact line 86