OAI/Analysis/KadisonKastler/PositiveConeStateEstimate.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The state norm estimate from an orthogonal positive decomposition

This is the last step of Araki's Theorem 4(8), Pacific J. Math. 50 (1974), 309–354. A reflection in the support of the positive part witnesses the state norm. The existence of the orthogonal decomposition is left explicit.

  1. theorem OAI.KadisonKastler.norm_sq_le_vectorState_norm_of_projection line 25
  2. theorem OAI.KadisonKastler.positiveCone_norm_sq_le_state_norm_of_decomposition line 74