Documentation

Mathlib.RingTheory.Polynomial.ShiftedLegendre

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.

Reference #

Tags #

shifted Legendre polynomials, derivative

source
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.

Equations
Instances For
    source
    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.

    source
    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.

    source
    @[simp]
    theorem Polynomial.degree_shiftedLegendre (n : ℕ) :
    (shiftedLegendre n).degree = ↑n

    The degree of shiftedLegendre n is n.

    source
    @[simp]
    theorem Polynomial.natDegree_shiftedLegendre (n : ℕ) :
    (shiftedLegendre n).natDegree = n
    source
    theorem Polynomial.neg_one_pow_mul_shiftedLegendre_comp_one_sub_X_eq (n : ℕ) :
    (-1) ^ n * (shiftedLegendre n).comp (1 - X) = shiftedLegendre n
    source
    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)ⁿ.