OAI/MathematicalPhysics/DefocusingNLS/Profile/RadialInnerShootingFamily.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

The canonical nonlinear inner family and its continuous complex boundary map.

  1. def OAI.DefocusingNLS.radialInnerShootingThreshold line 11
  2. theorem OAI.DefocusingNLS.radialInnerShootingData_exists line 13
  3. def OAI.DefocusingNLS.radialShootingInnerData line 20
  4. theorem OAI.DefocusingNLS.radialShootingInnerData_p line 23
  5. theorem OAI.DefocusingNLS.radialShootingInnerData_R line 27
  6. theorem OAI.DefocusingNLS.radialShootingInnerData_lo line 31
  7. theorem OAI.DefocusingNLS.radialShootingInnerData_c line 35
  8. theorem OAI.DefocusingNLS.radialShootingInnerData_b line 39
  9. def OAI.DefocusingNLS.radialShootingInnerAmplitude line 43
  10. theorem OAI.DefocusingNLS.radialShootingInnerAmplitude_spec line 46
  11. def OAI.DefocusingNLS.radialShootingInnerComplex line 52
  12. def OAI.DefocusingNLS.radialShootingInnerBoundary line 57
  13. theorem OAI.DefocusingNLS.continuous_radialShootingInnerBoundary line 61