OAI/MathematicalPhysics/DefocusingNLS/Linear/ExpandingInteractionPicture.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The forced expanding-torus evolution in the interaction picture

The exact free inverse turns a mild solution with continuous forcing into an ordinary Banach-valued primitive, without any extra spatial derivatives.

  1. theorem OAI.DefocusingNLS.expandingDuhamel_pullback line 19
  2. theorem OAI.DefocusingNLS.expandingMild_pullback line 42
  3. theorem OAI.DefocusingNLS.hasDerivAt_expandingMild_pullback line 59