OAI/MathematicalPhysics/DefocusingNLS/Linear/SobolevForwardMaximal.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Forward strong solutions are restrictions of the maximal flow

The local backward branch is glued using the right derivative provided by the endpoint Duhamel identity. The forward input needs no derivative at zero.

  1. theorem OAI.DefocusingNLS.forwardStrongSobolevSolution_restricts_maximal line 16