OAI/Analysis/Crouzeix/ContourHomotopy.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Contour Homotopy.

  1. def OAI.CrouzeixHilbert.operatorHomotopy line 20
  2. theorem OAI.CrouzeixHilbert.operatorHomotopy_zero line 23
  3. theorem OAI.CrouzeixHilbert.operatorHomotopy_one line 26
  4. theorem OAI.CrouzeixHilbert.numericalClosure_operatorHomotopy_subset line 29
  5. def OAI.CrouzeixHilbert.homotopyResolvent line 39
  6. theorem OAI.CrouzeixHilbert.homotopy_resolvent_isUnit line 42
  7. theorem OAI.CrouzeixHilbert.continuousOn_homotopyResolvent line 51
  8. theorem OAI.CrouzeixHilbert.commute_homotopyResolvent line 64
  9. theorem OAI.CrouzeixHilbert.hasDerivAt_homotopyResolvent line 78
  10. theorem OAI.CrouzeixHilbert.hasDerivAt_homotopyResolvent_path line 97
  11. theorem OAI.CrouzeixHilbert.continuousOn_homotopyResolvent_path line 110
  12. def OAI.CrouzeixHilbert.homotopyKernel line 119
  13. theorem OAI.CrouzeixHilbert.continuousOn_homotopyKernel line 123
  14. theorem OAI.CrouzeixHilbert.intervalIntegrable_homotopyKernel_left line 132
  15. theorem OAI.CrouzeixHilbert.intervalIntegrable_homotopyKernel_right line 142
  16. theorem OAI.CrouzeixHilbert.integral_homotopyKernel_left line 152
  17. theorem OAI.CrouzeixHilbert.hasDerivAt_homotopyKernel_primitive line 165
  18. theorem OAI.CrouzeixHilbert.integral_homotopyKernel_right line 178
  19. theorem OAI.CrouzeixHilbert.integral_integral_homotopyKernel line 187
  20. theorem OAI.CrouzeixHilbert.integral_resolvent_homotopy line 205
  21. theorem OAI.CrouzeixHilbert.ring_inverse_algebraMap line 229
  22. theorem OAI.CrouzeixHilbert.contourEval_one line 240