OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralWKBPhaseOrder.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The action is monotone after choosing the orientation of the WKB pair. For an oscillatory branch the choice depends only on the sign of gamma.

  1. theorem OAI.DefocusingNLS.spectralComplexSqrt_re_pos line 12
  2. theorem OAI.DefocusingNLS.spectralComplexSqrt_im_sign line 25
  3. theorem OAI.DefocusingNLS.spectralWKBPhase_monotone line 36