OAI/MathematicalPhysics/DefocusingNLS/Linear/ExpandingContinuousStep.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A continuous actual nonlinear step for varying scale and initial data

The already proved uniform small-data construction now yields a jointly continuous selected trajectory and endpoint remainder. Uniqueness of the small trajectory makes this independent of the existence proof's choices.

  1. theorem OAI.DefocusingNLS.exists_expandingContinuous_step line 20