OAI/MathematicalPhysics/DefocusingNLS/Profile/SlowInitialEquation.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The regularized slow solution on the initial half-planes

The regularized integral satisfies the differential equation and derivative shift identity on the initial complex half-planes.

  1. theorem OAI.DefocusingNLS.regularizedSlowSolution_eventuallyEq_euler line 15
  2. theorem OAI.DefocusingNLS.hasDerivAt_regularizedSlowSolution_initial line 24
  3. theorem OAI.DefocusingNLS.hasDerivAt_deriv_regularizedSlowSolution_initial line 32
  4. theorem OAI.DefocusingNLS.regularizedSlowSolution_kummer_equation_initial line 51

    Source documentation

    Kummer's equation for the actual regularized definition on the initial complex half-planes.

    theorem regularizedSlowSolution_kummer_equation_initial (q : ℂ) (m : ℕ) (x : ℂ)
    (hq : 0 < q.re) (hx : 0 < x.re) :
    x * deriv (deriv (regularizedSlowSolution q m)) x +
      ((m : ℂ) - x) * deriv (regularizedSlowSolution q m) x -
      q * regularizedSlowSolution q m x = 0 := by
…

    Mentions: OAI.DefocusingNLS.regularizedSlowSolution

  5. theorem OAI.DefocusingNLS.hasDerivAt_regularizedSlowSolution_shift_initial line 66

    Source documentation

    The derivative shift identity, before continuation to Re(q) > -1.

    theorem hasDerivAt_regularizedSlowSolution_shift_initial (q : ℂ) (m : ℕ) (x : ℂ)
    (hq : 0 < q.re) (hx : 0 < x.re) :
    HasDerivAt (regularizedSlowSolution q m)
      (-q * regularizedSlowSolution (q + 1) (m + 1) x) x := by
…

    Mentions: OAI.DefocusingNLS.regularizedSlowSolution