OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousComplexPotential.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The actual two-channel linearized potential

Physical evaluation of the complexified real derivative gives exactly the circular coefficient matrix used in the spectral ODE.

  1. theorem OAI.DefocusingNLS.circularComplexification_scalar line 17
  2. theorem OAI.DefocusingNLS.homogeneousComplexReal_physical line 44
  3. theorem OAI.DefocusingNLS.homogeneousComplexImag_physical line 51
  4. theorem OAI.DefocusingNLS.homogeneousComplexifiedPotential_physical line 58