OAI/MathematicalPhysics/DefocusingNLS/Profile/RadialFreeRiccati.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The logarithmic derivative of the actual free exterior and its real Riccati system.

  1. def OAI.DefocusingNLS.radialFreeRaw line 11
  2. def OAI.DefocusingNLS.radialFreeLog line 14
  3. theorem OAI.DefocusingNLS.radialFreeRaw_hasDerivAt line 17
  4. theorem OAI.DefocusingNLS.radialFreeRaw_hasDerivAt_deriv line 25
  5. theorem OAI.DefocusingNLS.radial_free_log_riccati line 50
  6. theorem OAI.DefocusingNLS.radialFreeLog_eq_j line 62
  7. theorem OAI.DefocusingNLS.radial_riccati_components line 72