OAI/Analysis/OperatorAlgebra/UnitaryMeanExpectation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Real-action averaging of a cpc projection onto an invariant von Neumann algebra gives a cpc projection onto its fixed-point algebra. This follows Anantharaman-Delaroche, Pacific J. Math. 171 (1995), Proposition 3.6, p. 329.

  1. theorem OAI.WeakPureInfiniteness.realAction_fixedPoint_expectation line 18