OAI/MathematicalPhysics/DefocusingNLS/Profile/RadialSmoothRamp.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

A twice differentiable replacement for the squared positive part in core/shell barriers.

  1. def OAI.DefocusingNLS.radialRampInner line 11
  2. def OAI.DefocusingNLS.radialRampInnerD line 14
  3. def OAI.DefocusingNLS.radialRampInnerDD line 17
  4. def OAI.DefocusingNLS.radialSmoothRamp line 20
  5. def OAI.DefocusingNLS.radialSmoothRampD line 23
  6. def OAI.DefocusingNLS.radialSmoothRampDD line 26
  7. theorem OAI.DefocusingNLS.hasDerivAt_radialRampInner line 29
  8. theorem OAI.DefocusingNLS.hasDerivAt_radialRampInnerD line 44
  9. theorem OAI.DefocusingNLS.hasDerivAt_radialSmoothRamp line 57
  10. theorem OAI.DefocusingNLS.hasDerivAt_radialSmoothRampD line 68