OAI/MathematicalPhysics/DefocusingNLS/Linear/ExpandingStepLipschitz.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Lipschitz remainder after a fixed nonlinear step

Subtracting the homogeneous linearized difference leaves only the difference of the quadratic sources. The resulting constant depends on the fixed step length and profile bound, and is uniform in the starting torus radius.

  1. theorem OAI.DefocusingNLS.exists_expandingNonlinearStep_difference_error line 16