OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralTurningAiryNonzero.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual outgoing comparison has a nonzero Airy limit. The cutoff is chosen from the explicit WKB error before extracting a subsequence.

  1. theorem OAI.DefocusingNLS.spectralTurning_outgoing_airy_nonzero line 12