SlowDerivativeAsymptotics.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

All-order expansions after any fixed spatial differentiation

theorem OAI.DefocusingNLS.normalized_iteratedDeriv_regularizedSlowSolution line 14

Source documentation

Normalizing the exact derivative leaves the same outgoing integral with shifted parameters, multiplied by the Pochhammer coefficient.

theorem normalized_iteratedDeriv_regularizedSlowSolution (k : ℕ) (q : ℂ) (m : ℕ) (x : ℂ)
    (hq : -1 < q.re) (hx : 0 ≤ x.re) (hx0 : x ≠ 0) :
    x ^ (q + k) * iteratedDeriv k (regularizedSlowSolution q m) x =
      ((-1 : ℂ) ^ k * (ascPochhammer ℂ k).eval q) *
        normalizedSlowSolution (q + k) (m + k) x := by
…

Mentions: OAI.DefocusingNLS.regularizedSlowSolution, OAI.DefocusingNLS.normalizedSlowSolution

theorem OAI.DefocusingNLS.iteratedDeriv_regularizedSlowSolution_allOrders_remainder line 25

Source documentation

The expansion and error control survive any fixed number of spatial derivatives, uniformly up to the imaginary rays.

theorem iteratedDeriv_regularizedSlowSolution_allOrders_remainder (k n : ℕ)
    (q : ℂ) (m : ℕ) (hq : -1 < q.re) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ x : ℂ, 0 ≤ x.re → 1 ≤ ‖x‖ →
      ‖x ^ (q + k) * iteratedDeriv k (regularizedSlowSolution q m) x -
        ((-1 : ℂ) ^ k * (ascPochhammer ℂ k).eval q) *
          slowAsymptoticPolynomial (q + k) (m + k) n x‖ ≤ C / ‖x‖ ^ (n + 1) := by
…

Mentions: OAI.DefocusingNLS.regularizedSlowSolution, OAI.DefocusingNLS.slowAsymptoticPolynomial