OAI/Analysis/KadisonKastler/SwappedBoundaryMean.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Transporting the scalar mean to the second coordinate

  1. def OAI.KadisonKastler.scalarSwapFamilyL line 18
  2. theorem OAI.KadisonKastler.scalarSwapFamilyL_norm_le line 22
  3. theorem OAI.KadisonKastler.scalarSwapFamilyL_const line 31
  4. theorem OAI.KadisonKastler.scalarSwapFamilyL_module line 36
  5. theorem OAI.KadisonKastler.scalarSwapFamilyL_translate line 44
  6. def OAI.KadisonKastler.swappedScalarBoundaryMean line 55
  7. def OAI.KadisonKastler.NonsingularAction.rightOnProduct line 89
  8. def OAI.KadisonKastler.randomWalkSecondScalarMean line 101
  9. theorem OAI.KadisonKastler.randomWalkSecondScalarMean_natural line 107