OAI/Analysis/KadisonKastler/PositiveReferenceCone.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Changing the cyclic reference inside the same positive cone

The quadratic positivity and the generated cone are unchanged when the reference is replaced by a cyclic vector in that cone. These are the reference-transport facts needed for projection-family amplification.

  1. theorem OAI.KadisonKastler.positiveCone_quadratic_nonneg line 30
  2. theorem OAI.KadisonKastler.positiveCone_change_reference_le line 37
  3. theorem OAI.KadisonKastler.positiveCone_change_reference_eq line 47