OAI/MathematicalPhysics/DefocusingNLS/Linear/ExpandingFiniteLocalExistence.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Local nonlinear existence on an arbitrary fixed similarity slab

Only a Lipschitz bound on a fixed state ball is used. Small initial data and small forcing keep the exponentially weighted fixed point in that ball.

  1. theorem OAI.DefocusingNLS.exists_expandingMild_local_finiteSlab line 17