OAI/MathematicalPhysics/DefocusingNLS/Profile/RadialAngularDensity.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Regular weighted angular coefficients at the radial origin.

  1. def OAI.DefocusingNLS.radialAngularDensity line 11
  2. def OAI.DefocusingNLS.radialAngularSlope line 14
  3. def OAI.DefocusingNLS.radialMatchedVelocityRatio line 18
  4. theorem OAI.DefocusingNLS.radialAngularDensity_continuous line 21
  5. theorem OAI.DefocusingNLS.radialAngularDensity_hasDerivAt line 28
  6. theorem OAI.DefocusingNLS.radialMatchedVelocityRatio_continuousOn line 43
  7. theorem OAI.DefocusingNLS.radialMatchedVelocity_eq_mul_ratio line 55
  8. theorem OAI.DefocusingNLS.radialAngularFlux_hasDerivAt line 58