OAI/MathematicalPhysics/DefocusingNLS/Linear/ExpandingPerturbationReaction.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Exact nonlinear perturbation and quadratic forcing

The perturbation of the actual odd-power equation splits into its profile linearization and its Taylor remainder. The estimates are uniform in the expanding torus radius and are the nonlinear ingredients of nl:step.

  1. def OAI.DefocusingNLS.expandingPerturbationReaction line 16
  2. def OAI.DefocusingNLS.expandingPerturbationSource line 35
  3. theorem OAI.DefocusingNLS.expandingPerturbationSource_apply line 46
  4. theorem OAI.DefocusingNLS.expandingPerturbationReaction_split line 56
  5. theorem OAI.DefocusingNLS.exists_expandingPerturbationSource_bound line 69
  6. theorem OAI.DefocusingNLS.exists_expandingPerturbationSource_lipschitz line 92