OAI/Analysis/KadisonKastler/ScalarShiftCesaro.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Contractive Cesaro averages for the nonsingular boundary shift

  1. def OAI.KadisonKastler.scalarShiftCesaro line 18
  2. theorem OAI.KadisonKastler.scalarShiftCesaro_apply line 22
  3. theorem OAI.KadisonKastler.scalarPullback_power_norm_le line 27
  4. theorem OAI.KadisonKastler.scalarShiftCesaro_norm_le line 35
  5. theorem OAI.KadisonKastler.scalarShiftCesaro_difference line 50
  6. theorem OAI.KadisonKastler.scalarShiftCesaro_difference_norm_le line 65
  7. theorem OAI.KadisonKastler.scalarShiftCesaro_fixed line 71