OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralRemoteIncomingDecay.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The qualitative incoming decay used to remove the endpoint at infinity. Solving the incoming equation for its large, invertible leading term gains two powers at every step, including every fixed logarithmic derivative.

  1. theorem OAI.DefocusingNLS.HasLogJetBound.eventually_congr line 13
  2. theorem OAI.DefocusingNLS.spectralRemote_incoming_gain line 28
  3. theorem OAI.DefocusingNLS.spectralRemote_incoming_iterate line 47
  4. theorem OAI.DefocusingNLS.HasLogJetBound.tendsto_zero line 65