OAI/MathematicalPhysics/DefocusingNLS/Profile/NormalizedSlowDerivative.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The differential recurrence of the normalized outgoing solution

  1. def OAI.DefocusingNLS.normalizedSlowSolution line 11
  2. theorem OAI.DefocusingNLS.hasDerivAt_normalizedSlowSolution line 14
  3. theorem OAI.DefocusingNLS.normalizedSlowSolution_bounded line 44

    Source documentation

    The normalized solution is uniformly bounded for large arguments in the closed right half-plane, including the two imaginary rays.

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

    Mentions: OAI.DefocusingNLS.normalizedSlowSolution