OAI/Analysis/KadisonKastler/NormalMarginalAgreement.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Recovering full product agreement from normal marginals

The two states may be nonnormal on the ambient operator algebra. Their normal marginals suffice to pass from the smoothed products to all products.

  1. theorem OAI.KadisonKastler.productVectorState_square line 21
  2. theorem OAI.KadisonKastler.normal_marginal_product_agreement line 28