OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralTurningProjectionLimit.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual forbidden-side WKB projection converges to the Airy growing projection, including its amplitude and logarithmic derivative correction.

  1. theorem OAI.DefocusingNLS.spectralTurning_growing_projection_margin line 13