OAI/MathematicalPhysics/DefocusingNLS/Nonlinear/CutoffProfilePhysicalLimit.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The sampled cutoff coefficient agrees locally with the whole-space profile

  1. theorem OAI.DefocusingNLS.sampledCutoffProfile_physical_eq line 16
  2. theorem OAI.DefocusingNLS.tendsto_sampledCutoffProfile_physical line 39
  3. theorem OAI.DefocusingNLS.tendsto_sampledCutoffProfilePath_physical line 55