OAI/MathematicalPhysics/DefocusingNLS/Profile/RadialShootingInnerEquation.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The selected shooting profile solves the actual stationary equation on the inner ball.

  1. def OAI.DefocusingNLS.radialShootingA line 11
  2. theorem OAI.DefocusingNLS.radialShootingInner_power_pos line 14
  3. theorem OAI.DefocusingNLS.radialShootingInner_c_eq line 20
  4. theorem OAI.DefocusingNLS.radialShootingInnerComplex_eq line 26
  5. theorem OAI.DefocusingNLS.radialShootingInner_positive line 32
  6. theorem OAI.DefocusingNLS.radialShootingInner_differentiable line 38
  7. theorem OAI.DefocusingNLS.radialShootingInner_origin line 48
  8. theorem OAI.DefocusingNLS.radialShootingInner_norm line 54
  9. theorem OAI.DefocusingNLS.radialShootingInner_stationary line 60