OAI/MathematicalPhysics/DefocusingNLS/Nonlinear/StableGraphRecurrence.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The fixed sequence solves the original two recurrences

The backward sum telescopes in the neutral coordinate as well as in the strictly expanding coordinates. Removing the 2^n weights recovers the forward and unstable-coordinate equations and gives actual endpoint decay.

  1. theorem OAI.DefocusingNLS.stableBackward_recurrence line 19
  2. theorem OAI.DefocusingNLS.stableBackward_unweighted_recurrence line 43
  3. theorem OAI.DefocusingNLS.stableForward_unweighted_recurrence line 56