OAI/Analysis/KadisonKastler/StrongInvariantState.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Strongly invariant states by Poisson smoothing

This proves the smoothing step of Marrakchi, arXiv:1811.10253v2, Proposition 3.10. Preservation of a prescribed nonnormal restriction is only asserted here on operators whose orbits are norm continuous.

  1. theorem OAI.KadisonKastler.poissonActionAverage_orbit_continuous line 24
  2. theorem OAI.KadisonKastler.exists_strongly_invariant_state line 44