OAI/MathematicalPhysics/DefocusingNLS/Nonlinear/CutoffStableBlowup.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Finite-time blowup of the constructed stable cutoff orbits

The conclusion retains the stable initial coordinates. The additional physical parameter argument is needed to obtain an open set of initial data.

  1. theorem OAI.DefocusingNLS.sampledCutoffProfileOrbit_center line 19
  2. theorem OAI.DefocusingNLS.cutoffGlobal_blowup line 34
  3. theorem OAI.DefocusingNLS.exists_cutoffStable_blowup line 64