OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralWKBFrame.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

An explicit WKB frame with constant Wronskian, for the scalar transfer on either side of the turning interval.

  1. def OAI.DefocusingNLS.spectralWKBValue line 11
  2. def OAI.DefocusingNLS.spectralWKBState line 13
  3. theorem OAI.DefocusingNLS.spectralWKBValue_product line 16
  4. theorem OAI.DefocusingNLS.spectralWKBState_wronskian line 23
  5. theorem OAI.DefocusingNLS.spectralWKBValue_hasDerivAt line 33
  6. theorem OAI.DefocusingNLS.spectralWKBState_hasDerivAt line 43