OAI/Analysis/KadisonKastler/ModularProductState.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A strongly invariant state with the two modular product marginals

For the actual cyclic separating representation of a type III factor, the left and right algebras are simple and conjugate. The constructed product state therefore has a strongly invariant extension to all ambient operators. This is the product-state step of Marrakchi, arXiv:1811.10253v2, Section 6.

  1. theorem OAI.KadisonKastler.ModularConjugationData.commutant_simple line 26
  2. theorem OAI.KadisonKastler.unitaryConj_mem_commutant_of_normalizes line 32
  3. theorem OAI.KadisonKastler.exists_modular_product_state_of_simple line 45
  4. theorem OAI.KadisonKastler.exists_typeIII_modular_product_state line 66