OAI/MathematicalPhysics/DefocusingNLS/Profile/RadialMatchedBoundary.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Actual physical inner and outer boundary values and derivatives agree.

  1. def OAI.DefocusingNLS.radialPhysicalExterior line 11
  2. def OAI.DefocusingNLS.radialPhysicalExteriorSlope line 14
  3. theorem OAI.DefocusingNLS.radialPhysicalExterior_hasDerivAt line 17
  4. def OAI.DefocusingNLS.radialShootingExteriorProfile line 34
  5. theorem OAI.DefocusingNLS.radialShootingExteriorProfile_ne_zero line 39
  6. theorem OAI.DefocusingNLS.radialShootingExteriorProfile_differentiableAt line 47
  7. theorem OAI.DefocusingNLS.radialMatchingMap_zero_boundary line 56
  8. theorem OAI.DefocusingNLS.exists_radial_inner_outer_boundary_match line 96