OAI/Analysis/KadisonKastler/StrongProductStateExtension.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Strongly invariant extensions with normal marginals

This is the normal-marginal specialization of Marrakchi, arXiv:1811.10253v2, Lemma 4.1 and Proposition 3.10. The initial product state is an explicit hypothesis; its construction is a separate step.

  1. theorem OAI.KadisonKastler.exists_strongly_invariant_with_normal_marginals line 24
  2. theorem OAI.KadisonKastler.exists_strongly_invariant_product_state line 61