OAI/Analysis/ModularTheory/AmplifiedModularAction.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The right modular action normalizes the concrete amplification, and the modular crossed product is contained in its fixed-point algebra.

  1. lemma OAI.WeakPureInfiniteness.modular_sigma_mem_commutant line 19
  2. lemma OAI.WeakPureInfiniteness.modularRightTranslation_pointwise_conjugate line 28
  3. lemma OAI.WeakPureInfiniteness.amplifiedModularAlgebra_invariant line 50
  4. lemma OAI.WeakPureInfiniteness.modularCore_mem_amplification line 68
  5. lemma OAI.WeakPureInfiniteness.modularCore_fixed_right line 75