OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralLiouvilleFrequencyJet.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Momentum jets for the actual scalar Liouville frequency on either side of its turn.

  1. def OAI.DefocusingNLS.spectralLiouvilleSlope line 10
  2. def OAI.DefocusingNLS.spectralLiouvilleSecond line 13
  3. theorem OAI.DefocusingNLS.spectralLiouvilleSlope_hasDerivAt line 16
  4. def OAI.DefocusingNLS.spectralLiouvilleMomentum line 28
  5. theorem OAI.DefocusingNLS.spectralLiouvilleMomentum_hasDerivAt line 32
  6. theorem OAI.DefocusingNLS.spectralLiouvilleMomentumSlope_hasDerivAt line 42