OAI/Analysis/ModularTheory/AmplifiedModularExpectation.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

An actual expectation onto the infinite scalar amplification of the standard von Neumann algebra of a nuclear quotient. It is obtained from the proved commutant projection in the amplified representation and pointwise Tomita conjugation, rather than from an unproved normal tensor extension.

  1. def OAI.WeakPureInfiniteness.amplifiedModularAlgebra line 21
  2. lemma OAI.WeakPureInfiniteness.mem_amplifiedModularAlgebra line 25
  3. theorem OAI.WeakPureInfiniteness.nuclear_quotient_amplified_expectation line 40