OAI/MathematicalPhysics/DefocusingNLS/Profile/RadialMatchedMultiplierLimit.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The mass and transport multipliers of the actual matched family.

  1. def OAI.DefocusingNLS.radialMatchedMassFunction line 12
  2. def OAI.DefocusingNLS.radialMatchedTransportFunction line 15
  3. def OAI.DefocusingNLS.radialMatchedFreeMassFunction line 18
  4. def OAI.DefocusingNLS.radialMatchedFreeTransportFunction line 21
  5. theorem OAI.DefocusingNLS.radialMatchedMassFunction_continuous line 24
  6. theorem OAI.DefocusingNLS.radialMatchedTransportFunction_continuous line 30
  7. theorem OAI.DefocusingNLS.radialMatchedFreeMassFunction_continuous line 45
  8. theorem OAI.DefocusingNLS.radialMatchedFreeTransportFunction_continuous line 48
  9. theorem OAI.DefocusingNLS.radialMatched_massMultiplier_tendsto line 53
  10. theorem OAI.DefocusingNLS.radialMatched_transportMultiplier_tendsto line 63