OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralScalarHalfLineExistence.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Compatible finite-interval solutions give a comparison solution on the entire right half-line. No uniform bound on the coefficient is needed.

  1. theorem OAI.DefocusingNLS.spectralScalar_halfLine_exists line 11