OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralFreeSlowJet.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The outgoing H solution in every angular mode of the free spectral equation.

  1. def OAI.DefocusingNLS.spectralFreeSlowJet line 11
  2. theorem OAI.DefocusingNLS.spectralFreeSlowJet_hasDerivAt line 15
  3. theorem OAI.DefocusingNLS.spectralFreeAngularJet_hasDerivAt line 51
  4. theorem OAI.DefocusingNLS.spectralFreeAngularPhysical_hasDerivAt line 65