OAI/MathematicalPhysics/DefocusingNLS/Linear/ExpandingSlabTrajectory.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Joining actual nonlinear similarity slabs

The finite paths here solve the polynomial equation at the correctly advanced radius. Their endpoint identity produces a global path solving that same equation on every finite interval.

  1. theorem OAI.DefocusingNLS.expandingGluedSlabs_local line 18
  2. theorem OAI.DefocusingNLS.expandingGluedSlabs_picard line 63