OAI/Analysis/KadisonKastler/TomitaPositivePairing.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Positivity of the modular quadratic vectors

The two commuting positive graph roots give the positive core pairing for the constructed polar conjugation. No natural-cone axiom is assumed.

  1. theorem OAI.KadisonKastler.tomitaPolarConjugation_positive_pairing line 24
  2. theorem OAI.KadisonKastler.tomitaPolarConjugation_quadratic_nonneg line 37