OAI/MathematicalPhysics/DefocusingNLS/Linear/ExpandingStepMapContinuity.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The continuous nonlinear endpoint map with its quantitative remainder

This combines the exact nonlinear-step estimates and parameter continuity for the same selected trajectories. Shrinking the input ball keeps every selected trajectory inside the fixed state ball used by the local theory.

  1. theorem OAI.DefocusingNLS.exists_expandingNonlinear_stepMap_continuous line 22