OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralWKBFluxMargin.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The selected oscillatory WKB branch has flux of the outgoing sign. The derivative smallness already used for transfer supplies a fixed margin.

  1. theorem OAI.DefocusingNLS.spectralComplexSqrt_re_two_thirds line 11
  2. theorem OAI.DefocusingNLS.spectralWKB_log_flux_margin line 25