OAI/MathematicalPhysics/DefocusingNLS/Profile/RadialTranslationSpectralMode.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The actual translation mode, including its weighted top derivative and nonvanishing at a positive radius.

  1. theorem OAI.DefocusingNLS.radialMatchedEvenProfile_deriv_nonzero line 16
  2. theorem OAI.DefocusingNLS.iteratedDeriv_conjugate line 44

    Also declared: OAI/MathematicalPhysics/DefocusingNLS/Profile/RadialTimeSpectralMode.lean:45 (same declaration text).

  3. def OAI.DefocusingNLS.radialMatchedTranslationMode line 50