OAI/MathematicalPhysics/DefocusingNLS/Profile/RadialPhase.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Integration of the nonsingular radial phase velocity.

  1. theorem OAI.DefocusingNLS.continuous_radialVelocity line 10
  2. def OAI.DefocusingNLS.radialPhase line 16
  3. theorem OAI.DefocusingNLS.radialPhase_origin line 19
  4. theorem OAI.DefocusingNLS.radialPhase_hasDerivAt line 22
  5. theorem OAI.DefocusingNLS.radialPhase_differentiable line 29
  6. theorem OAI.DefocusingNLS.radialPhase_deriv_hasDerivAt line 33