OAI/MathematicalPhysics/DefocusingNLS/Nonlinear/CutoffGlobalOrbit.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

A global cutoff orbit from compatible nonlinear steps

The profile is the actual sampled cutoff of the smooth stationary function. Compatible step solutions with geometric perturbation bounds give a global nonlinear trajectory, with vanishing error relative to that same profile. The stable graph supplies these endpoint data in the subsequent application.

  1. def OAI.DefocusingNLS.sampledCutoffProfileAtRadius line 21
  2. def OAI.DefocusingNLS.sampledCutoffProfileOrbit line 28
  3. theorem OAI.DefocusingNLS.continuous_sampledCutoffProfileOrbit line 36
  4. theorem OAI.DefocusingNLS.sampledCutoffProfileOrbit_at line 49
  5. theorem OAI.DefocusingNLS.exists_cutoffGlobal_orbit_of_steps line 65