OAI/MathematicalPhysics/DefocusingNLS/Profile/RadialMatchingData.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Constructed analytic matching data for the actual finite-power profile.

  1. structure OAI.DefocusingNLS.RadialMatchingData line 15
  2. theorem OAI.DefocusingNLS.radialMatchingData_nonempty line 48
  3. def OAI.DefocusingNLS.RadialMatchingData.determinant line 66
  4. theorem OAI.DefocusingNLS.RadialMatchingData.determinant_analyticAt line 74
  5. theorem OAI.DefocusingNLS.RadialMatchingData.mode_zero line 91