OAI/Analysis/ModularTheory/CoreIntegrals.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Strong continuity and integrated regular translations in the concrete modular crossed product. These are actual operators on L²(ℝ,H), without a trace or semifiniteness assumption on the generated von Neumann algebra.

  1. lemma OAI.WeakPureInfiniteness.continuous_modularLpTranslate line 20
  2. def OAI.WeakPureInfiniteness.modularLpTranslateOperator line 28
  3. lemma OAI.WeakPureInfiniteness.modularLpTranslateOperator_apply line 33
  4. lemma OAI.WeakPureInfiniteness.modularLpTranslate_opNorm_le line 38
  5. def OAI.WeakPureInfiniteness.integratedModularTranslation line 45
  6. lemma OAI.WeakPureInfiniteness.integratedModularTranslation_apply line 53
  7. lemma OAI.WeakPureInfiniteness.integratedModularTranslation_norm_le line 58
  8. lemma OAI.WeakPureInfiniteness.integratedModularTranslation_mem line 66