OAI/MathematicalPhysics/DefocusingNLS/Linear/ExpandingProfileEnergy.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Exact energy balance for the constructed torus profile propagator

The forcing is the derivative of the actual odd-power nonlinearity at the given moving profile. The trajectory is the already constructed unique finite-slab solution, rather than an assumed energy solution.

  1. theorem OAI.DefocusingNLS.expandingProfileTrajectory_energy_balance line 19