OAI/Analysis/KadisonKastler/ModularPositiveCone.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The cone generated by modular quadratic vectors

The definition uses actual vectors a J a J ξ, finite positive combinations, and norm closure. Its invariance is algebraic. Positivity of the reference pairing is kept explicit here and proved for the polar Tomita conjugation in TomitaPositivePairing.

  1. def OAI.KadisonKastler.modularQuadratic line 23
  2. theorem OAI.KadisonKastler.modularQuadratic_mul line 26
  3. theorem OAI.KadisonKastler.modularQuadratic_star line 38
  4. def OAI.KadisonKastler.modularPositiveCone line 46
  5. theorem OAI.KadisonKastler.modularPositiveCone_isClosed line 49
  6. theorem OAI.KadisonKastler.modularQuadratic_mem_positiveCone line 52
  7. theorem OAI.KadisonKastler.zero_mem_modularPositiveCone line 56
  8. theorem OAI.KadisonKastler.modularQuadratic_preserves_positiveCone line 61
  9. def OAI.KadisonKastler.realInnerHalfspace line 76
  10. theorem OAI.KadisonKastler.modularPositiveCone_acute line 87
  11. theorem OAI.KadisonKastler.modularPositiveCone_eq_zero_of_neg_mem line 122