OAI/Analysis/KadisonKastler/NormContinuousStateAverage.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Evaluating states on norm-continuous orbit averages

After Gaussian smoothing, a state may be interchanged with the orbit integral even when the state is not normal. This is the bounded integration step in Marrakchi, arXiv:1811.10253v2, Proposition 3.10.

  1. theorem OAI.KadisonKastler.weightedOperatorIntegral_eq_integral line 21
  2. theorem OAI.KadisonKastler.functional_weightedOperatorIntegral line 38
  3. theorem OAI.KadisonKastler.invariant_functional_orbit_integral line 60
  4. theorem OAI.KadisonKastler.gaussianStateAverage_orbit_continuous line 74