OAI/Analysis/FreeWords/PolarBounds.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.KKPolarSupport.polarOp_ker line 39
  2. theorem OAI.KKPolarSupport.closedRange_invariant line 52
  3. theorem OAI.KKPolarSupport.polarOp_commute line 62
  4. def OAI.KKPolarSupport.opAbs line 93
  5. theorem OAI.KKPolarSupport.opAbs_selfadjoint line 95
  6. theorem OAI.KKPolarSupport.opAbs_mul_self line 97
  7. theorem OAI.KKPolarSupport.opAbs_norm line 108
  8. theorem OAI.KKPolarSupport.opAbs_commute line 116
  9. theorem OAI.KKPolarSupport.polar_decomposition line 122
  10. theorem OAI.KKPolarSupport.polar_decomposition_bounds line 153