OAI/Analysis/KadisonKastler/SimpleProductStateExtension.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Strongly invariant product states on commuting simple algebras

The initial product state is constructed by cyclic compression, then extended with normal marginals and strong invariance.

  1. theorem OAI.KadisonKastler.exists_ambient_product_state_of_simple line 20
  2. theorem OAI.KadisonKastler.exists_strongly_invariant_product_of_simple line 42