OAI/MathematicalPhysics/DefocusingNLS/Nonlinear/StableGraphForward.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The forward part of the weighted graph map

In weighted coordinates the stable recurrence has a factor two. Rescaling the unstable coordinates by a fixed constant makes the mixed block small. The resulting estimates use the product sup norm, equivalent to the sum norm in the manuscript and complete on the same weighted sequences.

  1. theorem OAI.DefocusingNLS.stableForward_term_bound line 20
  2. def OAI.DefocusingNLS.stableForward line 39
  3. theorem OAI.DefocusingNLS.stableForward_zero line 54
  4. theorem OAI.DefocusingNLS.stableForward_succ line 60
  5. theorem OAI.DefocusingNLS.stableForward_norm_le line 67
  6. theorem OAI.DefocusingNLS.stableForward_sub line 80
  7. theorem OAI.DefocusingNLS.stableForward_dist_le line 95