OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousClassicalLinearization.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Classical equations for actual linearized generator vectors

The potential here is the proved derivative of the odd-power nonlinearity on the faithful Y space. Neither a spatial smoothness assumption nor an independent differential-operator eigenvalue hypothesis is introduced.

  1. theorem OAI.DefocusingNLS.homogeneousLinearized_domain_classical line 20
  2. theorem OAI.DefocusingNLS.homogeneousLinearized_generator_classical line 36