OAI/MathematicalPhysics/DefocusingNLS/Certificates/FreeRadialProfile.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

The actual flat-core/free-exterior limiting profile and its matching derivative.

  1. def OAI.DefocusingNLS.freeProfileRadius line 11
  2. def OAI.DefocusingNLS.freeRadialExterior line 13
  3. def OAI.DefocusingNLS.freeRadialProfile line 17
  4. theorem OAI.DefocusingNLS.freeProfileRadius_pos line 20
  5. theorem OAI.DefocusingNLS.freeProfileRadius_sq line 23
  6. theorem OAI.DefocusingNLS.freeRadialExterior_at_radius line 28
  7. theorem OAI.DefocusingNLS.hasDerivAt_freeRadialExterior line 33
  8. theorem OAI.DefocusingNLS.hasDerivAt_freeRadialExterior_at_radius line 58
  9. theorem OAI.DefocusingNLS.hasDerivAt_freeRadialProfile_at_radius line 64
  10. theorem OAI.DefocusingNLS.hasDerivAt_freeRadialProfile_inside line 89
  11. theorem OAI.DefocusingNLS.hasDerivAt_freeRadialProfile_outside line 95
  12. theorem OAI.DefocusingNLS.differentiable_freeRadialProfile line 106
  13. theorem OAI.DefocusingNLS.freeRadialProfile_nonzero_on_disk line 116