shifted Legendre Polynomials

In this file, we define the shifted Legendre polynomials shiftedLegendre n for n : ℕ as a polynomial in ℤ[X]. We prove some basic properties of the Legendre polynomials.

• factorial_mul_shiftedLegendre_eq: The analogue of Rodrigues' formula for the shifted Legendre polynomials;
• shiftedLegendre_eval_symm: The values of the shifted Legendre polynomial at x and 1 - x differ by a factor (-1)ⁿ.

Reference

• https://en.wikipedia.org/wiki/Legendre_polynomials

Tags

shifted Legendre polynomials, derivative

noncomputable def Polynomial.shiftedLegendre (n : ℕ) : Polynomial ℤ

shiftedLegendre n is an integer polynomial for each n : ℕ, defined by: Pₙ(x) = ∑ k ∈ Finset.range (n + 1), (-1)ᵏ * choose n k * choose (n + k) n * xᵏ These polynomials appear in combinatorics and the theory of orthogonal polynomials.

theorem Polynomial.factorial_mul_shiftedLegendre_eq (n : ℕ) : ↑n.factorial * shiftedLegendre n = (⇑derivative)^[n] (X ^ n * (1 - X) ^ n)

The shifted Legendre polynomial multiplied by a factorial equals the higher-order derivative of the combinatorial function X ^ n * (1 - X) ^ n. This is the analogue of Rodrigues' formula for the shifted Legendre polynomials.

theorem Polynomial.coeff_shiftedLegendre (n k : ℕ) : (shiftedLegendre n).coeff k = (-1) ^ k * ↑(n.choose k) * ↑((n + k).choose n)

The coefficient of the shifted Legendre polynomial at k is (-1) ^ k * (n.choose k) * (n + k).choose n.

@[simp]

theorem Polynomial.degree_shiftedLegendre (n : ℕ) : (shiftedLegendre n).degree = ↑n

The degree of shiftedLegendre n is n.

@[simp]

theorem Polynomial.natDegree_shiftedLegendre (n : ℕ) : (shiftedLegendre n).natDegree = n

theorem Polynomial.neg_one_pow_mul_shiftedLegendre_comp_one_sub_X_eq (n : ℕ) : (-1) ^ n * (shiftedLegendre n).comp (1 - X) = shiftedLegendre n

theorem Polynomial.shiftedLegendre_eval_symm (n : ℕ) {R : Type u_1} [Ring R] (x : R) : (aeval x) (shiftedLegendre n) = (-1) ^ n * (aeval (1 - x)) (shiftedLegendre n)

The values of the Legendre polynomial at x and 1 - x differ by a factor (-1)ⁿ.