OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralWKBSqrtApproximation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The complex momentum differs from the positive real momentum by at most |gamma|/sqrt(x). This is the pointwise estimate behind the bounded action error.

  1. theorem OAI.DefocusingNLS.spectralComplexSqrt_re_nonneg line 11
  2. theorem OAI.DefocusingNLS.spectralComplexSqrt_approx line 15