OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralRemoteSymbol.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Uniform logarithmic symbols on escaping half-lines. Constants are shared by the parameter sequence, while each fixed derivative order can discard a finite initial segment. This is the quantifier order needed at the remote endpoint.

  1. structure OAI.DefocusingNLS.HasUniformLogJetBound line 14
  2. theorem OAI.DefocusingNLS.HasUniformLogJetBound.mono line 24
  3. theorem OAI.DefocusingNLS.HasUniformLogJetBound.eventually_small line 35
  4. theorem OAI.DefocusingNLS.HasUniformLogJetBound.deriv line 50
  5. theorem OAI.DefocusingNLS.HasUniformLogJetBound.add line 56
  6. theorem OAI.DefocusingNLS.HasUniformLogJetBound.neg line 72
  7. theorem OAI.DefocusingNLS.HasUniformLogJetBound.sub line 79