OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralLiouvilleShellEnergy.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The Liouville Cauchy data on a fixed shell are bounded by the physical radial H¹ density, with a constant independent of the spectral parameters.

  1. theorem OAI.DefocusingNLS.spectralLiouvilleFactor_norm_sq line 10
  2. theorem OAI.DefocusingNLS.spectralLiouvilleSlope_shell_bound line 15
  3. theorem OAI.DefocusingNLS.spectralLiouvilleState_slope_energy line 35