OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousSpectralLocalizationWKB.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Exact residual of the scalar WKB logarithmic derivative. The same identity covers both exponential and oscillatory outer intervals.

  1. def OAI.DefocusingNLS.homogeneousSpectralWKBLog line 10
  2. def OAI.DefocusingNLS.homogeneousSpectralWKBResidual line 13
  3. theorem OAI.DefocusingNLS.homogeneousSpectralWKBLog_identity line 16
  4. theorem OAI.DefocusingNLS.homogeneousSpectralWKBLog_hasDerivAt line 24
  5. theorem OAI.DefocusingNLS.homogeneousSpectralWKB_acceleration line 37
  6. theorem OAI.DefocusingNLS.homogeneousSpectralWKBResidual_norm line 48