OAI/Analysis/ModularTheory/TraceExplicitConjugation.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The tracial conjugation is the explicit Fourier-gauge conjugation on the whole modular Hilbert space, by normal-weight totality.

  1. def OAI.WeakPureInfiniteness.modularWeightAdjointSemilinear line 15
  2. lemma OAI.WeakPureInfiniteness.modularWeightAdjointSemilinear_apply line 22
  3. lemma OAI.WeakPureInfiniteness.modularTraceConjugation_eq_explicit line 26