OAI/Analysis/KadisonKastler/ShiftBoundaryScalarMaps.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Scalar maps between paths and the invariant boundary

The measurable-subspace isometry implements descent and inclusion on the actual L-infinity classes. In particular the constructed invariant projection gives a contraction from ambient functions to boundary functions.

  1. def OAI.KadisonKastler.scalarProjectionToBoundaryL line 22
  2. theorem OAI.KadisonKastler.scalarProjectionToBoundaryL_ae line 28
  3. theorem OAI.KadisonKastler.norm_scalarProjectionToBoundaryL line 33
  4. theorem OAI.KadisonKastler.norm_scalarProjectionToBoundaryL_le line 37
  5. def OAI.KadisonKastler.scalarBoundaryLiftL line 42
  6. theorem OAI.KadisonKastler.scalarBoundaryLiftL_ae line 48
  7. theorem OAI.KadisonKastler.norm_scalarBoundaryLiftL line 54
  8. theorem OAI.KadisonKastler.scalarBoundaryLiftL_injective line 59
  9. theorem OAI.KadisonKastler.scalarBoundaryLiftL_fixed line 66
  10. theorem OAI.KadisonKastler.scalarBoundaryLiftL_positive line 73
  11. theorem OAI.KadisonKastler.scalarProjectionToBoundaryL_lift line 79