OAI/MathematicalPhysics/DefocusingNLS/Nonlinear/CutoffNonlinearStep.lean
1 declarations, 0 contain sorry, 0 declared as axioms
The nonlinear step for the actual sampled cutoff profile
The fixed-step bounds follow from a smooth stationary profile with finitely many symbol estimates.
- theorem
OAI.DefocusingNLS.exists_cutoffNonlinear_stepline 19