OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralForbiddenBoundaryExclusion.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A regular nonzero defocusing eigenpair cannot have a sufficiently accurate inward outgoing boundary condition when both channels are forbidden.

  1. theorem OAI.DefocusingNLS.spectralForbidden_boundary_exclusion line 13