OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralRadialShellNormalization.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A unit full radial energy bounds every interior shell used for the high-frequency boundary argument.

  1. theorem OAI.DefocusingNLS.spectralRadialEnergy_shell_le line 11