OAI/Analysis/KadisonKastler/ProductBoundaryLifts.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Descent to the first boundary coordinate

The product invariant-range theorem supplies an actual L-infinity function on the product boundary, with unchanged norm. Thus the first-coordinate invariant projection descends as a bounded linear map.

  1. def OAI.KadisonKastler.firstBoundaryMap line 24
  2. theorem OAI.KadisonKastler.firstBoundaryMap_measurePreserving line 27
  3. theorem OAI.KadisonKastler.firstBoundaryMeasure_eq_trim line 32
  4. def OAI.KadisonKastler.firstBoundaryLiftL line 38
  5. theorem OAI.KadisonKastler.firstBoundaryLiftL_ae line 43
  6. theorem OAI.KadisonKastler.firstBoundaryLiftL_norm line 47
  7. theorem OAI.KadisonKastler.firstBoundaryLiftL_injective line 51
  8. theorem OAI.KadisonKastler.exists_firstBoundaryLift_of_measurable line 57
  9. structure OAI.KadisonKastler.FirstBoundaryProjection line 76
  10. theorem OAI.KadisonKastler.exists_firstBoundaryProjection line 83
  11. def OAI.KadisonKastler.firstBoundaryProjection line 106