OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralTurningFarPhase.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform phase integrals on both far intervals. The oscillatory bound uses exactly the remote scale 16 sqrt(max(ell+1,omega)) chosen in the paper.

  1. theorem OAI.DefocusingNLS.spectralTurning_positive_far_phase line 13
  2. theorem OAI.DefocusingNLS.spectralTurning_negative_far_phase line 47