OAI/Analysis/KadisonKastler/ProductStateMarginalChange.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Changing one marginal of a product state

A faithful GNS representation of one marginal allows any other state on that algebra to be extended to the GNS operator algebra. Pulling it back through the cyclic compression changes precisely that marginal of the product state.

  1. theorem OAI.KadisonKastler.gnsCompression_product line 24
  2. theorem OAI.KadisonKastler.exists_product_state_change_left line 44