OAI/Analysis/KadisonKastler/ScalarShiftLimit.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The invariant scalar limit of shift averages

One common ultrafilter yields a contractive linear limit of the Cesaro operators. The telescoping estimate and weak closure of the nonsingular pullback graph force every value of the limit to be shift invariant.

  1. theorem OAI.KadisonKastler.scalarShiftCesaro_difference_tendsto_zero line 23
  2. theorem OAI.KadisonKastler.scalarShiftCesaro_weak_limit_fixed line 33
  3. theorem OAI.KadisonKastler.exists_scalar_shift_limit line 58