OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralTurningPotentialBound.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The frequency height on the fixed turning annulus is controlled by its slope at the turning point. This bounds the near-turning phase integral.

  1. theorem OAI.DefocusingNLS.spectralTurning_potential_slope_bound line 10