OAI/Analysis/KadisonKastler/CanonicalPositiveCone.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Positivity of the cone for the constructed modular conjugation

The positive core pairing and the constructed commutant theorem make the generated cone acute. In particular its intersection with its negative is zero. Self-duality and representation of all normal states are not asserted.

  1. def OAI.KadisonKastler.canonicalModularPositiveCone line 24
  2. theorem OAI.KadisonKastler.tomitaPolarConjugation_right_mem line 27
  3. theorem OAI.KadisonKastler.canonicalModularPositiveCone_acute line 32
  4. theorem OAI.KadisonKastler.canonicalModularPositiveCone_eq_zero_of_neg_mem line 43