OAI/Analysis/KadisonKastler/SelfAdjointVectorCompactness.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Weak compactness of self-adjoint vector balls

The bounded real vector images used in the modular Radon--Nikodym argument are closed and convex in the Hilbert norm, by weak operator compactness.

  1. def OAI.KadisonKastler.wotSelfAdjointBall line 22

    Source documentation

    Self-adjoint contractions of the given algebra, with the weak operator topology.

    def wotSelfAdjointBall (M : VonNeumannAlgebra H) : Set (H →WOT[ℂ] H) :=
…
  2. theorem OAI.KadisonKastler.wotSelfAdjointBall_compact line 25
  3. theorem OAI.KadisonKastler.wotSelfAdjointBall_convex line 38
  4. def OAI.KadisonKastler.selfAdjointVectorImage line 53

    Source documentation

    A fixed real-linear transform of the vector ball.

    def selfAdjointVectorImage (M : VonNeumannAlgebra H) (Ω : H) (P : H →L[ℝ] H) : Set H :=
…
  5. theorem OAI.KadisonKastler.wotVector_realMap_weak_continuous line 56
  6. theorem OAI.KadisonKastler.selfAdjointVectorImage_closed line 69
  7. theorem OAI.KadisonKastler.selfAdjointVectorImage_convex line 82