OAI/Analysis/BoundedHochschild/RectangularWeakCompactness.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Weak operator compactness for bounded operators between the two Hilbert spaces of a completely bounded factorization.

  1. theorem OAI.BoundedHochschild.KadisonRingrose.exists_rectangular_weak_ultralimit line 19
  2. def OAI.BoundedHochschild.KadisonRingrose.rectangularWeakBall line 40
  3. theorem OAI.BoundedHochschild.KadisonRingrose.rectangularWeakBall_isCompact line 42
  4. theorem OAI.BoundedHochschild.KadisonRingrose.rectangularWeakBall_isClosed line 72