OAI/MathematicalPhysics/DefocusingNLS/Profile/RadialShootingEquation.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

A canonical family of actual radial solutions for the shooting argument.

  1. def OAI.DefocusingNLS.radialShootingAmplitude line 12
  2. theorem OAI.DefocusingNLS.differentiable_radialShootingAmplitude line 21
  3. theorem OAI.DefocusingNLS.differentiableAt_deriv_radialShootingAmplitude line 32
  4. theorem OAI.DefocusingNLS.radialShootingAmplitude_eq line 49
  5. theorem OAI.DefocusingNLS.radialShootingAmplitude_equation line 63
  6. theorem OAI.DefocusingNLS.continuous_radialShootingAmplitude_endpoint line 98