OAI/MathematicalPhysics/DefocusingNLS/Profile/RadialMatchedEvenProfile.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

A smooth nonvanishing extension of the actual profile to signed radii.

  1. def OAI.DefocusingNLS.radialMatchedEvenProfile line 13
  2. theorem OAI.DefocusingNLS.radialMatchedEvenProfile_eq line 16
  3. theorem OAI.DefocusingNLS.radialMatchedEvenProfile_nonneg line 21
  4. theorem OAI.DefocusingNLS.radialMatchedEvenProfile_contDiff line 25
  5. theorem OAI.DefocusingNLS.radialMatchedEvenProfile_ne_zero line 31
  6. theorem OAI.DefocusingNLS.radialMatchedEvenProfile_eventuallyEq line 38
  7. theorem OAI.DefocusingNLS.radialMatchedEvenProfile_stationary line 44