OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralRemoteMatchedSymbol.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The weighted-Sobolev outgoing selection theorem supplies the individual symbol hypothesis for actual matched-profile eigenpairs.

  1. theorem OAI.DefocusingNLS.spectralRemote_matched_eigenpair_symbol line 12