OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousCanonicalContour.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Canonical identity and eigenvalue exclusion for the contour complement

The identity retained here makes the already-constructed finite-dimensional complement available for generator eigenvalue classification.

  1. theorem OAI.DefocusingNLS.contourComplement_eigenvector_modulus line 15
  2. theorem OAI.DefocusingNLS.finiteRank_canonical_contour_decomposition line 34