OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralRemoteIntegratingFactor.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The scalar integrating factor for an incoming coordinate. Only the real part of the coefficient enters its norm, so the large imaginary root costs no power in this estimate.

  1. def OAI.DefocusingNLS.spectralRemoteIntegratingFactor line 13
  2. theorem OAI.DefocusingNLS.spectralRemoteIntegratingFactor_base line 16
  3. theorem OAI.DefocusingNLS.spectralRemoteIntegratingFactor_deriv line 20
  4. theorem OAI.DefocusingNLS.spectralRemoteIntegratingFactor_equation line 34
  5. theorem OAI.DefocusingNLS.spectralRemoteIntegratingFactor_bound line 42