OAI/MathematicalPhysics/DefocusingNLS/Linear/ExpandingMildStrong.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The moving-scale mild solution is a strong Sobolev solution

Pulling back the exact weights identifies the changing spaces with the radius-one Fourier space. The resulting curve satisfies the physical Schrödinger equation with the expected two-derivative loss.

  1. theorem OAI.DefocusingNLS.hasDerivAt_expandingMild_strong line 17