OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralActionGronwall.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Remove the same-channel action before applying Gronwall. This keeps the integral of the WKB residual, rather than the length of the whole shell.

  1. theorem OAI.DefocusingNLS.spectral_action_gronwall line 11