OAI/Analysis/ModularTheory/FixedPointExpectation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The concrete cpc fixed-point projection for the modular right action. It fixes the entire crossed product. The converse fixed-point inclusion is deliberately not assumed or concluded here.

  1. theorem OAI.WeakPureInfiniteness.nuclear_quotient_modular_fixedPoint_expectation line 23