OAI/Analysis/KadisonKastler/PositiveConeReference.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Changing the reference inside the generated positive cone

A positive reference vector generates a subcone of the original cone. An invertible quadratic change of reference generates exactly the same cone; the inverse quadratic action proves the reverse inclusion.

  1. theorem OAI.KadisonKastler.modularPositiveCone_mono_reference line 19
  2. theorem OAI.KadisonKastler.modularPositiveCone_eq_of_mutual_reference line 32
  3. theorem OAI.KadisonKastler.modularPositiveCone_invertible_quadratic line 41