OAI/MathematicalPhysics/DefocusingNLS/Linear/ExpandingPerturbationEquation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The nonlinear perturbation equation is the actual Schrödinger mild equation

Subtracting a forced profile gives exactly the reaction used in the nonlinear step estimates. Conversely, adding that profile to a perturbation solution reconstructs an unforced nonlinear mild solution.

  1. theorem OAI.DefocusingNLS.expandingPerturbation_add_mild line 19
  2. theorem OAI.DefocusingNLS.expandingPerturbation_sub_mild line 59