OAI/Analysis/KadisonKastler/PositiveConeDualProjection.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Projection onto the generated positive cone

The Hilbert projection theorem gives a positive part and an orthogonal residual in the dual cone. Both vectors are fixed by the conjugation.

  1. theorem OAI.KadisonKastler.exists_positiveCone_dual_decomposition line 22