OAI/MathematicalPhysics/DefocusingNLS/Profile/NormalizedSlowIdentification.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Identification of the nonsingular tail with division by q

  1. theorem OAI.DefocusingNLS.shiftedSlowDerivative_parameter_step line 11
  2. theorem OAI.DefocusingNLS.shiftedSlowSecondDerivative_parameter_step line 18
  3. theorem OAI.DefocusingNLS.slowDerivative_coefficient_parameter_step line 32
  4. theorem OAI.DefocusingNLS.slowSecondDerivative_coefficient_parameter_step line 44
  5. theorem OAI.DefocusingNLS.q_mul_normalizedSlowB line 56
  6. theorem OAI.DefocusingNLS.q_mul_normalizedSlowC line 64
  7. theorem OAI.DefocusingNLS.q_mul_normalizedSlowCoefficient line 76