OAI/MathematicalPhysics/DefocusingNLS/Profile/RadialMatchedSmooth.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The matched radial profile is smooth and stationary at every positive radius.

  1. def OAI.DefocusingNLS.radialMatchedJet line 14
  2. theorem OAI.DefocusingNLS.radialMatchedJet_fst line 18
  3. theorem OAI.DefocusingNLS.radialMatchedJet_hasDerivAt line 24
  4. theorem OAI.DefocusingNLS.radialMatchedJet_contDiffOn line 40
  5. theorem OAI.DefocusingNLS.radialMatchedProfile_contDiffOn line 47
  6. theorem OAI.DefocusingNLS.radialMatchedProfile_hasDerivAt line 55
  7. theorem OAI.DefocusingNLS.radialMatchedProfile_stationary line 65