OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralWKBReflectedError.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Propagate the growing WKB coefficient from the turning edge toward a fixed inner radius by reflecting the actual Cauchy equation.

  1. theorem OAI.DefocusingNLS.spectralWKB_reflected_action_error line 13
  2. theorem OAI.DefocusingNLS.spectralWKB_reflected_residual_integral line 78
  3. theorem OAI.DefocusingNLS.spectralWKB_reflected_phase line 89