OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralWKBSingleBranch.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Separate the selected WKB branch from the true solution. The two errors are the integrated residual and the mismatch of the prescribed terminal data.

  1. theorem OAI.DefocusingNLS.spectralWKB_single_branch_error line 13