OAI/Analysis/KadisonKastler/SelfAdjointPolarTest.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The polar support test for self-adjoint vectors

The positive spectral support gives a self-adjoint unitary whose pairing with a self-adjoint operator is the sum of its positive and negative parts.

  1. theorem OAI.KadisonKastler.selfAdjoint_polar_test line 26