OAI/MathematicalPhysics/DefocusingNLS/Profile/SlowLaguerreTail.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The two Laguerre tails of the actual slow solution

The finite-part definitions make the initial values explicit. Integration by parts identifies them with coefficients of the first and second derivatives.

  1. def OAI.DefocusingNLS.slowLaguerreCoefficient line 15
  2. def OAI.DefocusingNLS.slowLaguerreB line 18
  3. def OAI.DefocusingNLS.slowLaguerreC line 21
  4. theorem OAI.DefocusingNLS.shiftedSlowDerivative_coefficient_step line 24
  5. theorem OAI.DefocusingNLS.slowLaguerreB_zero line 38
  6. theorem OAI.DefocusingNLS.slowLaguerreC_zero line 42
  7. theorem OAI.DefocusingNLS.slowLaguerreB_succ line 46
  8. theorem OAI.DefocusingNLS.slowLaguerreC_succ line 51
  9. theorem OAI.DefocusingNLS.slowLaguerreB_eq_derivative_coefficient line 56
  10. theorem OAI.DefocusingNLS.slowLaguerreC_eq_derivative_coefficients line 67