OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousCompactResolvent.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Compactness of the resolvent-contour perturbation

The compact-operator subspace is closed. Integrating a continuous curve in that subspace therefore still gives a compact operator. The second resolvent identity applies this fact to the exact compact perturbation of the time step.

  1. theorem OAI.DefocusingNLS.isCompactOperator_circleIntegral line 21
  2. theorem OAI.DefocusingNLS.circleResolventOperator_sub_isCompact line 41