OAI/MathematicalPhysics/DefocusingNLS/Nonlinear/OddPowerNonlinearity.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The odd-power defocusing nonlinearity

For an odd power p = 2m + 1, the scalar nonlinearity is a real polynomial in a complex variable and its conjugate. Its real derivative has the two circular components used in the linearized equation.

  1. def OAI.DefocusingNLS.oddPowerNonlinearity line 21
  2. theorem OAI.DefocusingNLS.oddPowerNonlinearity_eq line 23
  3. def OAI.DefocusingNLS.oddPowerDerivative line 34
  4. theorem OAI.DefocusingNLS.hasFDerivAt_oddPowerNonlinearity line 39
  5. theorem OAI.DefocusingNLS.contDiff_oddPowerNonlinearity line 48