OAI/Analysis/KadisonKastler/HermitianPositiveDecomposition.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Norm-additive positive decomposition of a Hermitian functional

The real Hahn–Banach pair construction already in the library gives the positive and negative parts with the exact total norm needed by Sakai's extreme-functional argument.

  1. theorem OAI.KadisonKastler.exists_norm_additive_positive_decomposition line 24