OAI/Analysis/KadisonKastler/MarginalStateMultiplication.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Multiplication bounds from a normal vector-state marginal

A state on the ambient operator algebra need not be normal. Agreement with a vector state on one algebra is enough for the corresponding one-sided multiplication estimate.

  1. theorem OAI.KadisonKastler.state_left_mul_le_of_vector_marginal line 22
  2. theorem OAI.KadisonKastler.state_right_mul_le_of_vector_marginal line 49