OAI/Analysis/KadisonKastler/RelativePowersStormer.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The state-to-vector estimate in a finite-matrix relative commutant

The positive parts remain in the central-vector space. Their support reflection belongs to the relative algebra, so its restricted state norm already controls the ambient vector distance.

  1. theorem OAI.KadisonKastler.relative_positiveCone_norm_sq_le_state_norm line 25