OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralCrossFluxLimit.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The pressure-free cross bound makes the total flux negligible on the square-root frequency scale.

  1. theorem OAI.DefocusingNLS.spectralCross_sqrt_frequency_limit line 11
  2. theorem OAI.DefocusingNLS.spectralCross_total_flux_limit line 26