OAI/Analysis/KadisonKastler/MinimalSpatialImplementer.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Minimum distance for bounded self-adjoint spatial implementers

The bounded family of self-adjoint implementers of the same derivation is weak-operator compact. Its distance from the self-adjoint part of the algebra is attained. This is the compactness step of Sakai's spatial splitting argument (Ann. Math. 83 (1966), Lemma 2, p.274).

  1. theorem OAI.KadisonKastler.wot_isSelfAdjoint_isClosed line 22
  2. theorem OAI.KadisonKastler.wot_norm_lowerSemicontinuous line 34
  3. theorem OAI.KadisonKastler.wot_vonNeumann_isClosed line 40
  4. def OAI.KadisonKastler.boundedSelfAdjointImplementers line 67
  5. theorem OAI.KadisonKastler.boundedSelfAdjointImplementers_compact line 71
  6. theorem OAI.KadisonKastler.exists_minimal_selfAdjoint_spatial_implementer line 86