OAI/MathematicalPhysics/DefocusingNLS/Certificates/HighAngularRayDecay.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Exponential decay on the actual outgoing rays, with a polynomial weight.

  1. theorem OAI.DefocusingNLS.highRay_norm_bounds line 12
  2. theorem OAI.DefocusingNLS.highRay_envelope_tendsto_zero line 26
  3. theorem OAI.DefocusingNLS.highRay_gaugedSlowSolution_decay line 56
  4. theorem OAI.DefocusingNLS.highRay_gaugedSlowSolution_derivative_decay line 64