OAI/Analysis/KadisonKastler/SpatialIsometry.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Bounded maps and isometries between spatial Hilbert tensors

The rectangular tensor map respects composition and adjoints. In particular, the tensor of a closed-subspace inclusion is an isometry whose range projection is the spatial amplification of the original projection.

  1. theorem OAI.KadisonKastler.spatialLinearMap_ext line 27
  2. def OAI.KadisonKastler.spatialMap line 41
  3. theorem OAI.KadisonKastler.spatialMap_tmul line 45
  4. theorem OAI.KadisonKastler.spatialMap_comp line 50
  5. theorem OAI.KadisonKastler.spatialMap_id line 57
  6. def OAI.KadisonKastler.spatialIsometry line 64
  7. theorem OAI.KadisonKastler.spatialIsometry_toContinuousLinearMap line 68
  8. theorem OAI.KadisonKastler.spatialIsometry_tmul line 74
  9. theorem OAI.KadisonKastler.spatialMap_adjoint line 84
  10. def OAI.KadisonKastler.spatialSubspaceInclusion line 105
  11. theorem OAI.KadisonKastler.spatialSubspaceInclusion_projection line 109