OAI/Analysis/FreeWords/PolarGeometry.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KKPolarSupport.closedRange line 15
  2. instance OAI.KKPolarSupport.closedRange_complete line 17
  3. def OAI.KKPolarSupport.closedRangeMap line 20
  4. theorem OAI.KKPolarSupport.closedRangeMap_val line 24
  5. theorem OAI.KKPolarSupport.closedRangeMap_dense line 28
  6. def OAI.KKPolarSupport.polarOnRange line 33
  7. theorem OAI.KKPolarSupport.polarOnRange_apply line 36
  8. theorem OAI.KKPolarSupport.polarOnRange_norm line 43
  9. def OAI.KKPolarSupport.polarOp line 51
  10. theorem OAI.KKPolarSupport.polarOp_apply_range line 54
  11. theorem OAI.KKPolarSupport.polarOp_mul line 62
  12. theorem OAI.KKPolarSupport.polarOp_star_mul line 67
  13. theorem OAI.KKPolarSupport.polarOp_projection line 86
  14. theorem OAI.KKPolarSupport.polarOp_partial line 91