OAI/MathematicalPhysics/DefocusingNLS/Linear/FourierCoordinateDerivative.lean

Recovering a strong Fourier-space derivative from continuous coordinates

For the Schrödinger application the candidate derivative loses two Sobolev orders. Once that derivative is a continuous Hilbert-space curve, its coordinate identities imply the strong derivative by the fundamental theorem of calculus.