OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralMatchedCaseIIBoundary.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual Case II shell argument removes both boundary channels once the exact interior flux is small.

  1. theorem OAI.DefocusingNLS.spectralMatched_caseII_boundary_from_flux line 14