OAI/MathematicalPhysics/DefocusingNLS/Linear/ExpandingStepExistence.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A uniform small-data radius for a fixed nonlinear step

Both the initial perturbation and the profile forcing may be chosen in a single ball independent of the expanding torus radius. The resulting path bound is linear in their sizes.

  1. theorem OAI.DefocusingNLS.exists_expandingPerturbation_step_radius line 16