OAI/MathematicalPhysics/DefocusingNLS/Nonlinear/CutoffContinuousStep.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The continuous nonlinear step for the actual cutoff profile

The same family has the exact unforced mild equation, a continuous endpoint remainder, and the scale-dependent remainder estimates. The stationary profile and its finite symbol bounds are the hypotheses for the step estimates.

  1. theorem OAI.DefocusingNLS.exists_cutoffNonlinear_step_continuous line 24