OAI/Analysis/KadisonKastler/StateActionAverages.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Probability averages of the implemented modular action

These maps are defined by vector integration. They are contractions and preserve the reference vector state whenever the implementing group fixes the reference vector.

  1. def OAI.KadisonKastler.stateActionAverage line 24
  2. theorem OAI.KadisonKastler.stateActionAverage_norm_le line 30
  3. theorem OAI.KadisonKastler.stateActionAverage_one line 36
  4. def OAI.KadisonKastler.stateActionAverageMap line 44
  5. theorem OAI.KadisonKastler.stateActionAverage_mem line 76
  6. theorem OAI.KadisonKastler.stateActionAverage_vectorState line 85