OAI/MathematicalPhysics/DefocusingNLS/Profile/RadialCartesianFirstRegularity.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

First Cartesian regularity of the actual matched profile, including the origin.

  1. def OAI.DefocusingNLS.radialMatchedCartesian line 15
  2. theorem OAI.DefocusingNLS.radialMatchedCartesian_contDiff_one line 18