OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralWKBTerminalError.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Terminal transfer error for the constructed WKB frame on an oscillatory interval. The bounded real action is retained in the explicit constant.

  1. theorem OAI.DefocusingNLS.spectralWKB_terminal_error line 12