OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousResolventCircle.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

The resolvent contour operator

This is the contour operator on the circle used to split the actual linearized time step. Its action on eigenvectors is proved directly. Idempotence and finite rank are separate obligations; no spectral splitting is assumed here.

  1. theorem OAI.DefocusingNLS.commute_resolvent_of_commute line 25
  2. theorem OAI.DefocusingNLS.commute_resolvent_operator line 33
  3. theorem OAI.DefocusingNLS.resolvent_first_identity line 38
  4. theorem OAI.DefocusingNLS.resolvent_apply_eigenvector line 62
  5. def OAI.DefocusingNLS.circleResolventOperator line 80
  6. theorem OAI.DefocusingNLS.circleIntegrable_resolvent line 83
  7. theorem OAI.DefocusingNLS.circleResolventOperator_apply line 91
  8. theorem OAI.DefocusingNLS.circleIntegral_map_clm line 101
  9. theorem OAI.DefocusingNLS.circleResolventOperator_commute_of_commute line 109
  10. theorem OAI.DefocusingNLS.circleResolventOperator_commute line 130
  11. theorem OAI.DefocusingNLS.circleResolventOperator_eq_of_annulus line 135
  12. theorem OAI.DefocusingNLS.circleResolventOperator_eigenvector_inside line 156
  13. theorem OAI.DefocusingNLS.circleResolventOperator_eigenvector_outside line 176