OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralMatchingMatrix.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The four physical matching columns and their exact determinant criterion.

  1. def OAI.DefocusingNLS.spectralStateCoordinates line 12
  2. def OAI.DefocusingNLS.spectralMatchingColumns line 26
  3. def OAI.DefocusingNLS.spectralMatchingMatrix line 29
  4. def OAI.DefocusingNLS.spectralMatchingDeterminant line 32
  5. theorem OAI.DefocusingNLS.spectralMatchingDeterminant_ne_zero_iff line 35
  6. theorem OAI.DefocusingNLS.spectralMatchingDeterminant_zero_iff line 45