OAI/Analysis/ModularTheory/TracialRightAction.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The actual tracial right action on the modular Hilbert space.

  1. lemma OAI.WeakPureInfiniteness.modularCoreSquareWeight_right_mul_finite line 16
  2. def OAI.WeakPureInfiniteness.modularFiniteWeightRight line 27
  3. def OAI.WeakPureInfiniteness.modularFiniteWeightLeft line 34
  4. lemma OAI.WeakPureInfiniteness.modularFiniteWeightMap_left line 41
  5. def OAI.WeakPureInfiniteness.modularTraceAntiunitary line 48
  6. lemma OAI.WeakPureInfiniteness.modularTraceAntiunitary_involutive line 53
  7. def OAI.WeakPureInfiniteness.modularTracialRightAction line 57
  8. lemma OAI.WeakPureInfiniteness.modularTracialRightAction_norm_le line 62
  9. lemma OAI.WeakPureInfiniteness.modularTracialRightAction_vector line 68
  10. lemma OAI.WeakPureInfiniteness.modularTracialRightAction_commutes line 87
  11. lemma OAI.WeakPureInfiniteness.modularTracialRightProjection_strong line 105