OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralTurningOuterPhase.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Uniform real phase integrals on the complete outer intervals.

  1. theorem OAI.DefocusingNLS.phase_continuous line 11
  2. theorem OAI.DefocusingNLS.spectralTurning_positive_outer_phase line 21
  3. theorem OAI.DefocusingNLS.spectralTurning_negative_outer_phase line 55