OAI/Analysis/ModularTheory/TraceConjugation.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The genuine tracial conjugation on the actual modular Hilbert space. It is extended from star on the dense finite-weight domain.

  1. def OAI.WeakPureInfiniteness.modularFiniteWeightStar line 17
  2. lemma OAI.WeakPureInfiniteness.modularFiniteWeightStar_involutive line 28
  3. def OAI.WeakPureInfiniteness.modularFiniteWeightAdjoint line 34
  4. lemma OAI.WeakPureInfiniteness.modularFiniteWeightAdjoint_norm line 38
  5. def OAI.WeakPureInfiniteness.modularTraceConjugation line 43
  6. lemma OAI.WeakPureInfiniteness.modularTraceConjugation_vector line 51
  7. lemma OAI.WeakPureInfiniteness.modularTraceConjugation_involutive line 57