OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralRemoteEnergy.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Four-coordinate energy estimates for the remote evolution; the imaginary leading part cancels.

  1. def OAI.DefocusingNLS.spectralRemoteEnergy line 10
  2. def OAI.DefocusingNLS.spectralRemoteReal line 12
  3. def OAI.DefocusingNLS.spectralRemoteSkew line 15
  4. theorem OAI.DefocusingNLS.spectralRemoteEnergy_nonneg line 20
  5. theorem OAI.DefocusingNLS.spectralRemoteEnergy_lower line 23
  6. theorem OAI.DefocusingNLS.spectralRemoteEnergy_upper line 30
  7. theorem OAI.DefocusingNLS.spectralRemoteReal_bound line 38
  8. theorem OAI.DefocusingNLS.spectralRemoteReal_skew line 49
  9. theorem OAI.DefocusingNLS.spectralRemoteEnergy_hasDerivAt line 56
  10. theorem OAI.DefocusingNLS.spectralRemoteEnergy_skew_bound line 68