OAI/MathematicalPhysics/DefocusingNLS/Linear/ExpandingPerturbationContinuity.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Continuity of the actual nonlinear perturbation with varying scale

The profile, residual and initial perturbation may all vary continuously. Every bounded family solving the actual local polynomial equation is then continuous in the finite-slab norm. This applies to the small solutions already constructed by the uniform nonlinear step theorem.

  1. theorem OAI.DefocusingNLS.continuous_expandingRadiusCurve_family line 18
  2. theorem OAI.DefocusingNLS.continuous_expandingPerturbationReaction_family line 27
  3. theorem OAI.DefocusingNLS.continuous_expandingPerturbation_family line 48