OAI/MathematicalPhysics/DefocusingNLS/Certificates/ShiftedSlowSolution.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DefocusingNLS.shiftedSlowSolution line 9
2. theorem OAI.DefocusingNLS.shifted_argument_mem_slitPlane line 12
3. theorem OAI.DefocusingNLS.hasDerivAt_shiftedSlowSolution line 18
4. theorem OAI.DefocusingNLS.hasDerivAt_deriv_shiftedSlowSolution line 28
5. theorem OAI.DefocusingNLS.shiftedSlowSolution_laguerre_equation line 43

   Source documentation

   This is the equation projected onto Laguerre polynomials in the paper.

   theorem shiftedSlowSolution_laguerre_equation (q : ℂ) (M : ℕ) (s : ℂ) (t : ℝ)
       (hq : -1 < q.re) (hsre : s.re = 0) (hsim : s.im ≠ 0) (ht : 0 ≤ t) :
       (t : ℂ) * deriv (deriv (shiftedSlowSolution q (M + 1) s)) t +
         (1 - (t : ℂ)) * deriv (shiftedSlowSolution q (M + 1) s) t +
         (M : ℂ) * deriv (shiftedSlowSolution q (M + 1) s) t -
         s * (deriv (deriv (shiftedSlowSolution q (M + 1) s)) t -
           deriv (shiftedSlowSolution q (M + 1) s) t) -
         q * shiftedSlowSolution q (M + 1) s t = 0 := by
   …

   Mentions: OAI.DefocusingNLS.shiftedSlowSolution