Generalized Laguerre polynomials

The library uses the monic, sign-reversed normalization

P_n^{(\alpha)}(x) = n!\, L_n^{(\alpha)}(-x) = \sum_k \binom{n}{k} (\alpha+k+1)_{n-k}\, x^k,

so that the zeros are nonpositive. For $\alpha \geq -1$:

every $P_n^{(\alpha)}$ has only real, simple zeros, and they are strictly negative when $\alpha > -1$;
consecutive polynomials strictly interlace;
the family satisfies a Favard three-term recurrence.

For $\alpha > -1$ the family is also orthogonal on the positive half-line:

\int_0^\infty P_m^{(\alpha)}(-x)\, P_n^{(\alpha)}(-x)\, x^\alpha e^{-x}\, dx = 0 \qquad (m \neq n).

References

G. Szegő, Orthogonal Polynomials, American Mathematical Society Colloquium Publications 23 (1939), Chapter V. The general three-term theory is on the Favard page.

Theorems

Generalized Laguerre polynomials are real-rootedMain result

RealRooted.generalizedLaguerre_splitssource

theorem generalizedLaguerre_splits (n : ℕ) {α : ℝ} (hα : -1 ≤ α) :
    (generalizedLaguerre n α).Splits

Generalized Laguerre polynomials have negative roots for α > -1

RealRooted.generalizedLaguerre_roots_negsource

theorem generalizedLaguerre_roots_neg (n : ℕ) {α : ℝ} (hα : -1 < α) :
    ∀ r ∈ (generalizedLaguerre n α).roots, r < 0

Generalized Laguerre polynomials have simple roots

RealRooted.generalizedLaguerre_hasSimpleRootssource

theorem generalizedLaguerre_hasSimpleRoots (n : ℕ) {α : ℝ} (hα : -1 ≤ α) :
    HasSimpleRoots (generalizedLaguerre n α)

Consecutive generalized Laguerre polynomials interlace

RealRooted.generalizedLaguerre_strictInterl_succsource

theorem generalizedLaguerre_strictInterl_succ (n : ℕ) {α : ℝ} (hα : -1 ≤ α) :
    StrictInterl (generalizedLaguerre n α) (generalizedLaguerre (n + 1) α)

Generalized Laguerre polynomials satisfy a Favard recurrence

RealRooted.generalizedLaguerre_satisfiesFavardRecurrencesource

theorem generalizedLaguerre_satisfiesFavardRecurrence (α : ℝ) :
    SatisfiesFavardRecurrence
      (fun n ↦ generalizedLaguerre n α)
      (fun n ↦ generalizedLaguerreDiag n α)
      (fun n ↦ generalizedLaguerreSubdiag n α)

Generalized Laguerre polynomials are orthogonal on the half-line

RealRooted.generalizedLaguerre_integral_orthogonalsource

theorem generalizedLaguerre_integral_orthogonal
    {α : ℝ} (hα : -1 < α) {m n : ℕ} (hmn : m ≠ n) :
    (∫ x in Ioi 0,
      (generalizedLaguerre m α).eval (-x) *
        (generalizedLaguerre n α).eval (-x) *
          x ^ α * Real.exp (-x)) = 0

Generalized Laguerre polynomials

References

≔ Definitions

⊢ Theorems

Definitions

Theorems