OAI/MathematicalPhysics/DefocusingNLS/Profile/RadialFreeMatchingWronskian.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The exact free logarithmic mismatch at the fixed matching radius.

  1. theorem OAI.DefocusingNLS.radialFreeInnerJet_hasDerivAt line 12
  2. theorem OAI.DefocusingNLS.radialShootingRaw_ne_zero line 37
  3. def OAI.DefocusingNLS.radialFreeMatchingFactor line 50
  4. theorem OAI.DefocusingNLS.radialFreeInner_boundary_ne_zero line 56
  5. theorem OAI.DefocusingNLS.radialFreeMatchingFactor_ne_zero line 62
  6. theorem OAI.DefocusingNLS.radialFreeInner_logarithmic_mismatch line 78