OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralFirstClosedBoundary.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Exterior first-component tests give the remaining outer flux trace.

  1. theorem OAI.DefocusingNLS.spectralFirst_closedBoundary line 11