OAI/MathematicalPhysics/DefocusingNLS/Profile/SlowCompactAsymptotics.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform all-order asymptotics on compact parameter sets

  1. theorem OAI.DefocusingNLS.continuous_slowAsymptoticJet line 11
  2. theorem OAI.DefocusingNLS.regularizedSlowSolution_compact_allOrders_remainder line 22

    Source documentation

    The all-order remainder constant can be chosen uniformly on every compact subset of the regularized parameter half-plane Re(q)>-1.

    theorem regularizedSlowSolution_compact_allOrders_remainder (n m : ℕ) (Q : Set ℂ)
    (hQ : IsCompact Q) (hq : ∀ q ∈ Q, -1 < q.re) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ q ∈ Q, ∀ 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