OAI/Analysis/ModularTheory/TraceNormalConjugation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The actual tracial conjugation agrees with the explicit Fourier formula on normal-ordered finite-weight vectors. The identification uses two limits of the same Gaussian-regularized adjoint.

  1. lemma OAI.WeakPureInfiniteness.modularTracialRightGaussian_strong line 17
  2. lemma OAI.WeakPureInfiniteness.modularTraceConjugation_normal line 33