OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralWKBPhaseIntegral.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A phase integral controlled by the momentum derivative and endpoint size.

  1. theorem OAI.DefocusingNLS.spectralWKB_phase_integral line 10