OAI/MathematicalPhysics/DefocusingNLS/Profile/SlowAllOrdersAsymptotic.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

All-order outgoing asymptotics on the closed right half-plane

Taylor expansion of the actual compactified integral gives a remainder uniform in the argument, including the nonzero imaginary boundary.

  1. def OAI.DefocusingNLS.slowAsymptoticPolynomial line 16
  2. theorem OAI.DefocusingNLS.compactifiedSlowSolution_uniform_bound line 19
  3. theorem OAI.DefocusingNLS.taylorWithinEval_compactifiedSlowSolution line 33
  4. theorem OAI.DefocusingNLS.regularizedSlowSolution_allOrders_remainder line 46

    Source documentation

    For every finite order the normalized defining integral has a uniform inverse-power expansion, rather than just a formal series.

    theorem regularizedSlowSolution_allOrders_remainder (n : ℕ) (q : ℂ) (m : ℕ)
    (hq : -1 < q.re) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ x : ℂ, 0 ≤ x.re → 1 ≤ ‖x‖ →
      ‖normalizedSlowSolution q m x - slowAsymptoticPolynomial q m n x‖ ≤
        C / ‖x‖ ^ (n + 1) := by
…

    Mentions: OAI.DefocusingNLS.normalizedSlowSolution, OAI.DefocusingNLS.slowAsymptoticPolynomial