OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralCircularCoordinates.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Exact slow/fast coordinates for the circular spectral equation.

The choice has leading eigenvectors (1,0) and (1,-hi/2), as in the proof of spectrum.tex, Lemma spec:slow-basis. No asymptotic assertion is assumed in these coordinate identities.

  1. def OAI.DefocusingNLS.spectralCircularNu line 15
  2. def OAI.DefocusingNLS.spectralCircularFast line 18
  3. def OAI.DefocusingNLS.spectralCircularSlow line 21
  4. theorem OAI.DefocusingNLS.spectralCircular_reconstruct line 24
  5. theorem OAI.DefocusingNLS.spectralCircular_coordinate_derivatives line 38