OAI/Analysis/KadisonKastler/MarginalStateApproximation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Strong approximation of products under normal marginals

This estimates a possibly nonnormal ambient state using its vector-state marginals. It is the product approximation step of Marrakchi's Lemma 4.1.

  1. theorem OAI.KadisonKastler.state_product_sub_le_of_vector_marginals line 20
  2. theorem OAI.KadisonKastler.state_product_tendsto_of_vector_marginals line 33