OAI/MathematicalPhysics/DefocusingNLS/Linear/ExpandingMildEnergy.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Energy differentiation for the actual expanding mild equation

The proof takes place in the free interaction picture. The solution and forcing need only be continuous in the exact moving Sobolev norm.

  1. theorem OAI.DefocusingNLS.expanding_component_derivative line 19
  2. theorem OAI.DefocusingNLS.hasDerivAt_expandingMildEnergy line 72