OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralWKBSlopeError.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The WKB slope at the remote endpoint differs from the prescribed outgoing slope by the imaginary-potential error and the amplitude derivative.

  1. theorem OAI.DefocusingNLS.spectralWKB_oscillatory_slope_error line 11