OAI/Analysis/KadisonKastler/WOTDistanceSeparation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Weak operator separation and operator-norm distance

A dual estimate on weak-operator continuous functionals annihilating a closed subspace gives strict norm approximants in that subspace.

  1. def OAI.KadisonKastler.wotNormBall line 22
  2. theorem OAI.KadisonKastler.wotNormBall_compact line 24
  3. theorem OAI.KadisonKastler.wotNormBall_convex line 40
  4. theorem OAI.KadisonKastler.exists_near_subspace_of_wot_dual_bound line 53