OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralWKBResidualIntegral.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Integrated WKB error from exact momentum primitives. The constants only use derivative bounds and the momentum at the near endpoint.

  1. theorem OAI.DefocusingNLS.spectralWKB_residual_integral line 11