OAI/Analysis/ModularTheory/FixedPointIdentification.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Identification of the modular right-action fixed points with the actual crossed product, and the resulting concrete cpc core retraction.

  1. theorem OAI.WeakPureInfiniteness.convolutionSmoothed_mem_core line 19
  2. theorem OAI.WeakPureInfiniteness.modular_fixedPoint_mem_core line 38
  3. theorem OAI.WeakPureInfiniteness.modular_mem_core_iff line 52
  4. theorem OAI.WeakPureInfiniteness.nuclear_quotient_modular_core_expectation line 68