OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousLinearizedEnergy.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Energy balance for the actual linearized propagator

The continuous potential history used to construct the finite-slab flow gives exactly the energy pairing with the true odd-power derivative. This specialization retains the manuscript's two homogeneous energies.

  1. theorem OAI.DefocusingNLS.homogeneousLinearizedTrajectory_energy_balance line 19