OAI/Analysis/KadisonKastler/ParameterizedBoundaryMean.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The random-walk mean with an arbitrary probability parameter

The extra coordinate is left unchanged by the group. The construction is natural for every nonsingular map of that coordinate, which is the property needed when combining the two separate boundary means.

  1. def OAI.KadisonKastler.NonsingularAction.leftOnProduct line 24
  2. theorem OAI.KadisonKastler.NonsingularAction.leftOnProduct_apply line 33
  3. def OAI.KadisonKastler.randomWalkParameterizedScalarMean line 42
  4. theorem OAI.KadisonKastler.randomWalkParameterizedScalarMean_natural line 53