OAI/Analysis/KadisonKastler/L2TensorCoordinates.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Scalar tensor coordinates for iterated L2 spaces

The scalar-vector tensor map preserves inner products and has dense range. Swapping its two scalar factors therefore gives the L2 Fubini isometry needed for the modular Fourier calculation.

  1. def OAI.KadisonKastler.scalarLpTensor line 24
  2. theorem OAI.KadisonKastler.scalarLpTensor_apply_ae line 28
  3. theorem OAI.KadisonKastler.inner_scalarLpTensor line 33
  4. def OAI.KadisonKastler.l2TensorLinearMap line 46
  5. theorem OAI.KadisonKastler.l2TensorLinearMap_tmul line 50
  6. theorem OAI.KadisonKastler.inner_l2TensorLinearMap line 54
  7. def OAI.KadisonKastler.l2TensorEmbedding line 63
  8. theorem OAI.KadisonKastler.l2TensorEmbedding_dense line 67
  9. def OAI.KadisonKastler.l2ScalarSwap line 87
  10. theorem OAI.KadisonKastler.l2ScalarSwap_tensor line 95