OAI/MathematicalPhysics/DefocusingNLS/Profile/RadialExteriorShootingData.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Compact shooting data for simultaneous complex value and slope matching.

  1. def OAI.DefocusingNLS.radialShootingValue line 12
  2. def OAI.DefocusingNLS.radialShootingQ line 15
  3. def OAI.DefocusingNLS.radialShootingM line 18
  4. theorem OAI.DefocusingNLS.continuous_profileMatchingParameter line 22
  5. theorem OAI.DefocusingNLS.continuous_radialShootingValue line 25
  6. theorem OAI.DefocusingNLS.continuous_radialShootingQ line 29
  7. theorem OAI.DefocusingNLS.continuous_radialShootingM line 33
  8. theorem OAI.DefocusingNLS.radialShootingValue_norm line 37
  9. theorem OAI.DefocusingNLS.radialShootingM_ne_zero line 60
  10. theorem OAI.DefocusingNLS.radialShooting_free_value line 64
  11. theorem OAI.DefocusingNLS.radialShooting_free_annulus line 83