OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralRemoteActualCoefficients.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Individual symbols and endpoint formulas for the actual angular, spectral and odd-power coefficients.

  1. theorem OAI.DefocusingNLS.spectralRemote_leading_endpoint line 15
  2. theorem OAI.DefocusingNLS.spectralRemote_leading_individual line 27
  3. theorem OAI.DefocusingNLS.spectralRemote_physical_bounded_individual line 38
  4. theorem OAI.DefocusingNLS.spectralRemote_oddPower_individual line 53