OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralMatchedCaseIIBoundaryEnergy.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The normalized Case II shell gives a uniformly bounded physical Cauchy trace on a subsequence, with no boundary-data assumption.

  1. theorem OAI.DefocusingNLS.spectralMatched_caseII_boundary_energy line 13