OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralLiouvilleOscillatoryBounds.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Every subinterval of the oscillatory region has the same transfer bound. The phase and residual integrals are nonnegative and therefore restrict.

  1. theorem OAI.DefocusingNLS.spectralLiouville_oscillatory_subinterval line 11