OAI/MathematicalPhysics/DefocusingNLS/Profile/SlowLaguerreRecurrence.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The Laguerre recurrence for the actual regularized slow solution

  1. theorem OAI.DefocusingNLS.shiftedSlowDerivative_equation line 12
  2. theorem OAI.DefocusingNLS.integrableOn_weightedPolynomial_shiftedSlowDerivative line 27
  3. theorem OAI.DefocusingNLS.shiftedSlowDerivative_projected_equation line 35
  4. theorem OAI.DefocusingNLS.slowLaguerre_recurrence line 81

    Source documentation

    The recurrence in Lemma free:laguerre now holds for the integral-defined coefficients of H, with no spectral or sequence hypothesis.

    theorem slowLaguerre_recurrence (q : ℂ) (M : ℕ) (s : ℂ) (n : ℕ)
    (hq : -1 < q.re) (hsre : s.re = 0) (hsim : s.im ≠ 0) :
    (q + n) * slowLaguerreCoefficient q (M + 1) s n =
      -(M : ℂ) * slowLaguerreB q (M + 1) s (n + 1) -
        s * slowLaguerreC q (M + 1) s n := by
…

    Mentions: OAI.DefocusingNLS.slowLaguerreCoefficient, OAI.DefocusingNLS.slowLaguerreB, OAI.DefocusingNLS.slowLaguerreC