OAI/MathematicalPhysics/DefocusingNLS/Profile/RadialSpectralConjugation.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Conjugating and swapping the physical components reflects a radial mode across the real spectral axis and preserves all regular outgoing conditions.

  1. theorem OAI.DefocusingNLS.spectral_iteratedDeriv_star line 11
  2. theorem OAI.DefocusingNLS.harmonicRadialEigenpair_conjugate line 17
  3. def OAI.DefocusingNLS.RadialSpectralMode.conjugate line 34