OAI/Analysis/ModularTheory/DualUnitary.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

The character unitaries that implement the dual action of the real modular crossed product. The two covariance formulas are on actual L² operators; no dual weight or trace is postulated.

  1. lemma OAI.WeakPureInfiniteness.memLp_modularDual line 17
  2. def OAI.WeakPureInfiniteness.modularDual line 26
  3. lemma OAI.WeakPureInfiniteness.modularDual_ae line 29
  4. lemma OAI.WeakPureInfiniteness.modularDual_norm line 33
  5. lemma OAI.WeakPureInfiniteness.modularDual_add line 41
  6. lemma OAI.WeakPureInfiniteness.modularDual_smul line 49
  7. lemma OAI.WeakPureInfiniteness.modularDual_comp line 57
  8. lemma OAI.WeakPureInfiniteness.modularDual_zero line 65
  9. def OAI.WeakPureInfiniteness.modularDualUnitary line 71
  10. lemma OAI.WeakPureInfiniteness.modularDual_coefficient line 82
  11. lemma OAI.WeakPureInfiniteness.spectralCharacter_translation line 94
  12. lemma OAI.WeakPureInfiniteness.modularDual_translation line 104