OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralTurningAiryHalfLineLimit.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

One limiting Airy solution works on every fixed compact interval. Local uniqueness makes the independently obtained interval limits agree.

  1. theorem OAI.DefocusingNLS.spectralTurningAiry_halfLine_limit line 11