OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralLiouvilleOscillatoryPhase.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A bound for the whole positive-frequency phase, in either oscillatory orientation, follows from the real phase integral.

  1. theorem OAI.DefocusingNLS.spectralLiouville_positive_phase_bound line 11