OAI/Analysis/KadisonKastler/L2KernelSwap.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Kernel formulas for the L2 Fubini isometry

Testing against scalar tensors identifies the swap of any integrable kernel represented by its rows and columns. The application uses bounded phase and indicator kernels multiplied by two L2 vectors.

  1. theorem OAI.KadisonKastler.inner_scalarLpTensor_kernel line 22
  2. theorem OAI.KadisonKastler.l2ScalarSwap_of_kernel line 39
  3. theorem OAI.KadisonKastler.integrable_bounded_L2_kernel line 70