OAI/MathematicalPhysics/DefocusingNLS/Nonlinear/CutoffStepForcing.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The actual sampled cutoff supplies the nonlinear step data

The profile is a forced nonlinear mild solution. Its forcing is exactly minus i times the sampled cutoff residual, with the required uniform L^(-2-a) bound.

  1. theorem OAI.DefocusingNLS.exists_cutoffResidual_small_scale line 22
  2. def OAI.DefocusingNLS.sampledCutoffDefectPath line 32
  3. theorem OAI.DefocusingNLS.sampledCutoffProfile_forced_mild line 40
  4. theorem OAI.DefocusingNLS.exists_cutoffStep_profile_forcing_bounds line 67