feat(papers/NLSCritical): well-posedness of energy-critical NLS

[jvanwinden]

This PR adds an a priori estimate for the energy-critical nonlinear Schrodinger equation in spatial dimension 3. This estimate is strong enough to imply global well-posedness and scattering, but these properties are more complicated to state. The estimate was first proved in a landmark paper by Colliander, Keel, Staffilani, Takaoka, and Tao.

Regarding implementation:

• Since $u$ maps from $\mathbb{R}^3$ to $\mathbb{C}$, I had to use fderiv instead of $\nabla$ to write $|\nabla u|^2$. But the norm of the fderiv should still be exactly the right quantity.

[github-actions]

👋 This is an automated welcome message. 🤖
Thanks for the contributions!

A few friendly reminders while the review gets started:

• Please take a look at the style guidelines,
  especially the conventions for references, categories, AMS tags, and answer(sorry).
• You can manage some PR labels by leaving a comment with +label-name or -label-name; for example, +awaiting-author or -awaiting-author.
• This repository is mainly for formalised statements. Proofs longer than about 25-50 lines are usually out of scope; longer proofs are welcome to be included/linked via the formal_proof mechanism.

Thanks again for helping improve Formal Conjectures.