OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralWKBConstruction.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The scalar WKB frame is constructed from integrals, including its normalization. Its constant Wronskian and differential equation are derived.

  1. def OAI.DefocusingNLS.spectralWKBInitialAmplitude line 12
  2. def OAI.DefocusingNLS.spectralWKBPhase line 14
  3. def OAI.DefocusingNLS.spectralWKBFrame line 17
  4. theorem OAI.DefocusingNLS.spectralWKBInitialAmplitude_normalization line 22
  5. theorem OAI.DefocusingNLS.spectralWKBPhase_continuousOn line 30
  6. theorem OAI.DefocusingNLS.spectralWKBPhase_hasDerivAt line 38
  7. theorem OAI.DefocusingNLS.spectralWKBFrame_continuousOn line 43
  8. theorem OAI.DefocusingNLS.spectralWKBFrame_wronskian line 56
  9. theorem OAI.DefocusingNLS.spectralWKBFrame_hasDerivAt line 71