OAI/MathematicalPhysics/DefocusingNLS/Nonlinear/CutoffLocalExistence.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Exact local evolution near the sampled stationary cutoff

Finite symbol jets control the whole cutoff path and its true mild residual. The starting-scale smallness gives a genuine solution of the nonlinear equation, with no globally Lipschitz extension of that equation.

  1. theorem OAI.DefocusingNLS.exists_cutoffProfile_localSolution line 21