OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralParameterGrowthEquation.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

The coupled profile, outgoing column and differentiated column form a polynomial ten-coordinate ODE with coarse exponential derivative bounds.

  1. def OAI.DefocusingNLS.spectralParameterState line 16
  2. theorem OAI.DefocusingNLS.spectralParameterState_zero line 21
  3. theorem OAI.DefocusingNLS.spectralParameterState_one line 23
  4. theorem OAI.DefocusingNLS.spectralParameterState_two line 25
  5. theorem OAI.DefocusingNLS.spectralParameterState_three line 27
  6. theorem OAI.DefocusingNLS.spectralParameterState_four line 29
  7. theorem OAI.DefocusingNLS.spectralParameterState_five line 31
  8. theorem OAI.DefocusingNLS.spectralParameterState_six line 34
  9. theorem OAI.DefocusingNLS.spectralParameterState_seven line 36
  10. theorem OAI.DefocusingNLS.spectralParameterState_eight line 38
  11. theorem OAI.DefocusingNLS.spectralParameterState_nine line 40
  12. def OAI.DefocusingNLS.spectralParameterDifferential line 43
  13. theorem OAI.DefocusingNLS.spectralParameterDifferential_eval line 81
  14. theorem OAI.DefocusingNLS.spectralParameterState_hasDerivAt line 109
  15. theorem OAI.DefocusingNLS.spectralParameterState_bound line 139
  16. theorem OAI.DefocusingNLS.spectralParameter_derivatives_exponential_bound line 154