OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousEnergyObservation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Integrated local observation for the actual whole-space linear evolution

The constants depend on the fixed profile and k, and are independent of both initial data and slab length. The proof uses the previously established mild energy derivative, with no generator-domain hypothesis.

  1. theorem OAI.DefocusingNLS.homogeneousLinearized_integrated_observation line 21