OAI/MathematicalPhysics/DefocusingNLS/Profile/RadialTimeSpectralMode.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The actual nonzero radial time-translation spectral mode.

  1. theorem OAI.DefocusingNLS.radialMatchedEuler_nonzero line 14
  2. theorem OAI.DefocusingNLS.iteratedDeriv_conjugate line 45

    Also declared: OAI/MathematicalPhysics/DefocusingNLS/Profile/RadialTranslationSpectralMode.lean:44 (same declaration text).

  3. def OAI.DefocusingNLS.radialMatchedTimeMode line 51