OAI/Analysis/KadisonKastler/CountableSpatialTensor.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Countable sums commute with the spatial Hilbert tensor product

The coordinate tensor map preserves inner products on algebraic tensors. Its completion is onto because it contains every finitely supported tensor vector. This is the concrete amplification bridge for the constructed faithful cyclic representation.

  1. def OAI.KadisonKastler.countableTensorVector line 24
  2. theorem OAI.KadisonKastler.countableTensorVector_apply line 31
  3. def OAI.KadisonKastler.countableTensorBilinear line 35
  4. theorem OAI.KadisonKastler.inner_countableTensorVector line 49
  5. def OAI.KadisonKastler.countableTensorAlgebraic line 56
  6. theorem OAI.KadisonKastler.countableTensorAlgebraic_tmul line 60
  7. theorem OAI.KadisonKastler.inner_countableTensorAlgebraic line 63
  8. def OAI.KadisonKastler.countableTensorIsometry line 74
  9. theorem OAI.KadisonKastler.countableTensorIsometry_tmul line 79
  10. theorem OAI.KadisonKastler.countableTensorIsometry_surjective line 85
  11. def OAI.KadisonKastler.countableTensorEquiv line 113
  12. theorem OAI.KadisonKastler.countableTensorEquiv_tmul line 118
  13. theorem OAI.KadisonKastler.countableTensorEquiv_intertwines line 129

    Source documentation

    Amplifying either tensor factor and then distributing gives the diagonal amplification of its spatial action.

    theorem countableTensorEquiv_intertwines (a : H →L[ℂ] H) (b : K →L[ℂ] K)
    (z : SpatialHilbert (CountableHilbertSum H) K) :
    countableTensorEquiv (spatialTensorOp (l2Diagonal a) b z) =
      l2Diagonal (spatialTensorOp a b) (countableTensorEquiv z) := by
…

    Mentions: OAI.KadisonKastler.CountableHilbertSum, OAI.KadisonKastler.countableTensorEquiv, OAI.KadisonKastler.l2Diagonal