OAI/MathematicalPhysics/DefocusingNLS/Profile/RadialSmoothBarrierRegular.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Regularity and exact flat/quadratic pieces of the radial barriers.

  1. theorem OAI.DefocusingNLS.radialSmoothRamp_flat line 9
  2. theorem OAI.DefocusingNLS.radialSmoothRamp_quadratic line 13
  3. theorem OAI.DefocusingNLS.differentiable_radialLowerBarrier line 20
  4. theorem OAI.DefocusingNLS.differentiable_deriv_radialLowerBarrier line 24
  5. theorem OAI.DefocusingNLS.differentiable_radialInverseBarrier line 31
  6. theorem OAI.DefocusingNLS.differentiable_deriv_radialInverseBarrier line 35