OAI/MathematicalPhysics/DefocusingNLS/Nonlinear/CutoffResidualScaling.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Exact normalization of the cutoff residual

The residual has three terms. When p = 2m+1 and 2am = 1, all three have the common physical factor L^(-2-2a).

  1. theorem OAI.DefocusingNLS.oddPowerNonlinearity_real_mul line 19
  2. theorem OAI.DefocusingNLS.oddPowerNonlinearity_profile_scaling line 27
  3. def OAI.DefocusingNLS.cutoffResidual line 38
  4. def OAI.DefocusingNLS.normalizedCutoffResidual line 46
  5. theorem OAI.DefocusingNLS.cutoffResidual_scaling line 55