OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralQuotientDecay.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Outgoing columns divided by the profile satisfy the energy boundary decay criterion.

  1. theorem OAI.DefocusingNLS.spectralQuotientJet_bigO line 11
  2. theorem OAI.DefocusingNLS.spectralQuotient_energy_decay line 33