OAI/Analysis/KadisonKastler/ConjugationAveragedState.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Invariant states obtained by the constructed scalar mean

The scalar orbit of the state is averaged, so every invariant restriction is preserved even when the state is not normal. Strong invariance under probability-measure averages is a separate step.

  1. def OAI.KadisonKastler.ScalarInvariantMean.stateOrbitScalar line 27
  2. theorem OAI.KadisonKastler.ScalarInvariantMean.stateOrbitScalar_apply line 32
  3. def OAI.KadisonKastler.ScalarInvariantMean.stateOrbitMap line 35
  4. def OAI.KadisonKastler.ScalarInvariantMean.averagedState line 52
  5. theorem OAI.KadisonKastler.ScalarInvariantMean.averagedState_apply line 55
  6. theorem OAI.KadisonKastler.ScalarInvariantMean.averagedState_eq_of_invariant_values line 58
  7. theorem OAI.KadisonKastler.ScalarInvariantMean.averagedState_isState line 66
  8. theorem OAI.KadisonKastler.ScalarInvariantMean.averagedState_invariant line 88
  9. theorem OAI.KadisonKastler.ScalarInvariantMean.averagedState_fixed line 98