OAI/Analysis/KadisonKastler/SelfAdjointPolarCorrection.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Correcting an almost involutive selfadjoint element

The polar factor stays selfadjoint. A small square defect gives a linear norm bound, as required when rounding nearby reducing projections.

  1. theorem OAI.KadisonKastler.polar_unitary_selfAdjoint line 17
  2. theorem OAI.KadisonKastler.exists_selfAdjoint_unitary_of_square_defect line 40