OAI/MathematicalPhysics/DefocusingNLS/Nonlinear/StableGraphPointSources.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The actual projected point sources on weighted pair sequences

These definitions package the nonlinear remainder and the linear coordinate commutation defect. The extension is only outside the fixed sequence ball; inside that ball their values are exactly the endpoint sources.

  1. def OAI.DefocusingNLS.stableWeightedPairSource line 21
  2. theorem OAI.DefocusingNLS.stableWeightedPairSource_dist_le line 29
  3. theorem OAI.DefocusingNLS.stableWeightedPairSource_zero_bound line 41
  4. theorem OAI.DefocusingNLS.stableWeightedPairSource_value line 54
  5. def OAI.DefocusingNLS.stableFrameForwardSource line 67
  6. def OAI.DefocusingNLS.stableFrameCoordinateSource line 72
  7. theorem OAI.DefocusingNLS.stableFrameForwardSource_value line 79
  8. theorem OAI.DefocusingNLS.stableFrameCoordinateSource_value line 86
  9. theorem OAI.DefocusingNLS.stableFramePointSources_lipschitz line 97
  10. theorem OAI.DefocusingNLS.stableFramePointSources_zero line 123