OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralMatchedEscapeExclusion.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The two constructed cases exclude every escaping angular/frequency sequence of nonzero regular outgoing modes in the counting strip.

  1. theorem OAI.DefocusingNLS.spectralMatched_escape_exclusion line 14