OAI/Analysis/ModularTheory/RightTranslation.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The commuting right regular translations in the concrete modular representation. These are the commutant operators used to analyze the compression to scalar functions times the distinguished modular vector.

  1. def OAI.WeakPureInfiniteness.modularRightTranslation line 18
  2. lemma OAI.WeakPureInfiniteness.modularRightTranslation_ae line 22
  3. lemma OAI.WeakPureInfiniteness.modularRightTranslation_norm line 29
  4. lemma OAI.WeakPureInfiniteness.modularRightTranslation_comp line 44
  5. lemma OAI.WeakPureInfiniteness.modularRightTranslation_zero line 56
  6. def OAI.WeakPureInfiniteness.modularRightTranslationEquiv line 62
  7. lemma OAI.WeakPureInfiniteness.modularRightTranslation_star line 71
  8. lemma OAI.WeakPureInfiniteness.modularRightTranslation_coefficient line 77
  9. lemma OAI.WeakPureInfiniteness.modularRightTranslation_translate line 98
  10. lemma OAI.WeakPureInfiniteness.modularRightTranslation_star_translate line 116
  11. theorem OAI.WeakPureInfiniteness.modularRightTranslation_mem_commutant line 128

    Source documentation

    The right regular translations commute with the entire von Neumann closure, not only its displayed generators.

    theorem modularRightTranslation_mem_commutant (s : ℝ) :
    modularRightTranslation μ S.D s ∈ (modularCrossedProduct μ S).commutant := by
…

    Mentions: OAI.WeakPureInfiniteness.modularRightTranslation, OAI.WeakPureInfiniteness.modularCrossedProduct