OAI/Analysis/KadisonKastler/PositivePolarUnitary.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Positivity removes a state-preserving polar unitary

The positive core pairing makes the unitary times the bounded middle operator positive. Equality of the squares then determines that middle operator uniquely, and its dense range determines the unitary.

  1. theorem OAI.KadisonKastler.operator_nonneg_of_inner_nonneg line 24
  2. theorem OAI.KadisonKastler.positive_polar_unitary_eq_one line 35