OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousOutgoingPropagation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Propagating the outgoing plane back from a mode-dependent far radius

The ODE is linear on every positive closed annulus. A representation by the two outgoing columns at one far point therefore holds at the fixed radius used by the canonical boundary operator.

  1. theorem OAI.DefocusingNLS.physicalField_combination line 20
  2. theorem OAI.DefocusingNLS.physicalField_sub line 28
  3. theorem OAI.DefocusingNLS.homogeneousPhysicalOutgoingPlane_backward line 36
  4. theorem OAI.DefocusingNLS.homogeneousPhysicalOutgoingPlane_of_eventually line 62