OAI/MathematicalPhysics/DefocusingNLS/Profile/SlowKummerEquation.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DefocusingNLS.slowEulerKernel_adjacent line 11
2. theorem OAI.DefocusingNLS.slowEulerIntegral_adjacent line 37
3. theorem OAI.DefocusingNLS.slowEulerIntegral_contiguous line 47
4. theorem OAI.DefocusingNLS.regularizedSlowSolution_contiguous line 62
5. theorem OAI.DefocusingNLS.regularizedSlowSolution_shift_relation line 78
6. theorem OAI.DefocusingNLS.regularizedSlowSolution_kummer_equation line 100

   Source documentation

   Kummer's equation for the defining regularized integral throughout Re(q)>-1, with positive spatial real part.

   theorem regularizedSlowSolution_kummer_equation (q : ℂ) (m : ℕ) (x : ℂ)
       (hq : -1 < 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