OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralRemotePhysicalCoefficientScale.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The physical odd-power coefficients have a fixed decaying radial factor; the only residual phase frequency is twice the profile exponent's imaginary part.

  1. theorem OAI.DefocusingNLS.exponential_powers line 14
  2. theorem OAI.DefocusingNLS.spectralRemote_physical_coefficient_factors line 22
  3. theorem OAI.DefocusingNLS.spectralRemote_complex_exponential_symbol line 56