OAI/Analysis/KadisonKastler/ProjectionPinchedState.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Pinching a vector state across an almost central projection

This is the first state approximation in Haagerup's Lemma 3.6 (Acta Math.158(1987), p.138). The pinched state is constructed from two vector functionals and retains faithfulness. Its norm distance from the original state is controlled by the left/right projection gap.

  1. theorem OAI.KadisonKastler.vectorFunctional_norm_sub_le line 23
  2. def OAI.KadisonKastler.projectionReflection line 44
  3. theorem OAI.KadisonKastler.projectionReflection_unitary line 46
  4. def OAI.KadisonKastler.projectionPinchedState line 57
  5. theorem OAI.KadisonKastler.projectionPinchedState_reflection line 60
  6. theorem OAI.KadisonKastler.vectorFunctional_commuting_unitary line 72
  7. theorem OAI.KadisonKastler.projectionPinchedState_norm_sub_le line 82