OAI/MathematicalPhysics/DefocusingNLS/Linear/ExpandingStepMap.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The actual nonlinear endpoint map and its small Lipschitz remainder

For a bounded profile and small forcing, this constructs the nonlinear step map on one uniform initial-data ball. Its linear part is the actual profile-linearized evolution, with the quantitative remainder estimates required in the manuscript's nonlinear iteration.

  1. theorem OAI.DefocusingNLS.expandingPerturbation_unique_of_small line 18
  2. theorem OAI.DefocusingNLS.exists_expandingNonlinear_stepMap line 36