OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousLogJetBound.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Logarithmic bounds for the actual radial ODE coefficient recurrence

Differentiation in logarithmic radius preserves an exponential order. This small calculus is used for the finite recurrence of high radial derivatives.

  1. structure OAI.DefocusingNLS.HasLogJetBound line 19
  2. theorem OAI.DefocusingNLS.HasLogJetBound.mono line 28
  3. theorem OAI.DefocusingNLS.HasLogJetBound.const line 37
  4. theorem OAI.DefocusingNLS.HasLogJetBound.zero line 47
  5. theorem OAI.DefocusingNLS.HasLogJetBound.exponential line 52
  6. theorem OAI.DefocusingNLS.HasLogJetBound.neg line 78
  7. theorem OAI.DefocusingNLS.HasLogJetBound.add line 85
  8. theorem OAI.DefocusingNLS.HasLogJetBound.sub line 104
  9. theorem OAI.DefocusingNLS.HasLogJetBound.deriv line 108
  10. theorem OAI.DefocusingNLS.HasLogJetBound.smul line 114
  11. theorem OAI.DefocusingNLS.HasLogJetBound.mul line 132