Bessel polynomials

DefinitionBessel polynomial#✓fully proved

For a natural number \(n\), the \(n\)-th classical Bessel polynomial \(y_n\) is the polynomial with rational coefficients \(y_n(x) = \sum_{k=0}^{n} \frac{(n+k)!}{2^k \, k! \, (n-k)!} \, x^k\).

noncomputable def besselPolynomial (n : ℕ) : Polynomial ℚ :=
  ∑ k ∈ Finset.range (n + 1),
    Polynomial.C ((Nat.factorial (n + k) : ℚ) /
      ((2 ^ k : ℚ) * (Nat.factorial k : ℚ) * (Nat.factorial (n - k) : ℚ))) *
      (Polynomial.X ^ k)

Sources

• Schork, lines 285-288.

Used by 5

Used byExplicit formula for the Bessel polynomials · The first Bessel polynomial · The second Bessel polynomial · The zeroth Bessel polynomial · Expansion of \((XV)^n\) in Bessel numbers

TheoremExplicit formula for the Bessel polynomials#✓fully proved

For every natural number \(n\), the Bessel polynomial \(y_n \in \mathbb{Q}[x]\) equals \(\sum_{k=0}^{n} \frac{(n+k)!}{2^k \, k! \, (n-k)!} \, x^k\).

This is the defining formula, so the identity holds by definition.

theorem besselPolynomial_eq_sum (n : ℕ) :
    besselPolynomial n =
      ∑ k ∈ Finset.range (n + 1),
        Polynomial.C ((Nat.factorial (n + k) : ℚ) /
          ((2 ^ k : ℚ) * (Nat.factorial k : ℚ) * (Nat.factorial (n - k) : ℚ))) *
          (Polynomial.X ^ k)

Sources

• Schork, lines 285-288.

Uses 1

Statement usesBessel polynomial

TheoremThe zeroth Bessel polynomial#✓fully proved

The Bessel polynomial \(y_0\) is the constant polynomial \(1\).

theorem besselPolynomial_zero : besselPolynomial 0 = 1

Sources

• Schork, lines 285-288.

Uses 1

Statement usesBessel polynomial

TheoremThe first Bessel polynomial#✓fully proved

The Bessel polynomial \(y_1\) equals \(1 + x\).

theorem besselPolynomial_one :
    besselPolynomial 1 = Polynomial.C 1 + Polynomial.X

Sources

• Schork, lines 285-288.

Uses 1

Statement usesBessel polynomial

TheoremThe second Bessel polynomial#✓fully proved

The Bessel polynomial \(y_2\) equals \(1 + 3x + 3x^2\).

theorem besselPolynomial_two :
    besselPolynomial 2 =
      Polynomial.C 1 + Polynomial.C 3 * Polynomial.X +
        Polynomial.C 3 * (Polynomial.X ^ 2)

Sources

• Schork, lines 285-288.

Uses 1

Statement usesBessel polynomial

5 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.