OAI/Analysis/ModularTheory/RightContinuity.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Strong continuity of the concrete right-regular modular action.

  1. lemma OAI.WeakPureInfiniteness.isClosed_continuous_operator_orbit line 17
  2. lemma OAI.WeakPureInfiniteness.continuous_operator_apply_varying line 32
  3. lemma OAI.WeakPureInfiniteness.pointwise_modularUnitary_norm_le line 55
  4. lemma OAI.WeakPureInfiniteness.pointwise_modularUnitary_continuous line 63
  5. lemma OAI.WeakPureInfiniteness.modularRightTranslation_continuous line 80