OAI/MathematicalPhysics/DefocusingNLS/Profile/CompactifiedSlowDerivative.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A regular derivative recurrence at inverse radius zero

  1. theorem OAI.DefocusingNLS.hasDerivAt_compactifiedSlowSolution_pos line 14
  2. theorem OAI.DefocusingNLS.hasDerivWithinAt_compactifiedSlowSolution_zero line 36

    Source documentation

    The derivative at the endpoint is obtained from the actual normalized integral and its limit, not imposed as a formal asymptotic coefficient.

    theorem hasDerivWithinAt_compactifiedSlowSolution_zero (q : ℂ) (m : ℕ) (x : ℂ)
    (hq : -1 < q.re) (hx : 0 ≤ x.re) (hx0 : x ≠ 0) :
    HasDerivWithinAt (compactifiedSlowSolution q m x)
      (q * ((m : ℂ) - 1 - q) / x) (Ici 0) 0 := by
…

    Mentions: OAI.DefocusingNLS.compactifiedSlowSolution

  3. theorem OAI.DefocusingNLS.hasDerivWithinAt_compactifiedSlowSolution line 53