Legendre Polynomials

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

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

shiftedLegendre n is the polynomial defined in terms of derivatives of order n.

Equations

• Polynomial.shiftedLegendre n = Polynomial.C (↑n.factorial)⁻¹ * (⇑Polynomial.derivative)^[n] (Polynomial.X ^ n * (1 - Polynomial.X) ^ n)

theorem Polynomial.Finsum_iterate_deriv {R : Type u_1} [CommRing R] (k : ℕ) (h : ℕ → ℕ) : (⇑derivative)^[k] (∑ m ∈ Finset.range (k + 1), h m • (-1) ^ m * X ^ (k + m)) = ∑ m ∈ Finset.range (k + 1), h m • (-1) ^ m * (⇑derivative)^[k] (X ^ (k + m))

theorem Polynomial.shiftedLegendre_eq_sum (n : ℕ) : shiftedLegendre n = ∑ k ∈ Finset.range (n + 1), C ((-1) ^ k) * ↑(n.choose k) * ↑((n + k).choose n) * X ^ k

The expand of shiftedLegendre n.

theorem Polynomial.shiftedLegendre_eq_int_poly (n : ℕ) : ∃ (a : ℕ → ℤ), shiftedLegendre n = ∑ k ∈ Finset.range (n + 1), ↑(a k) * X ^ k

shiftedLegendre n is an integer polynomial.

theorem Polynomial.deriv_one_sub_X {n i : ℕ} : (⇑derivative)^[i] ((1 - X) ^ n) = (-1) ^ i * n.descFactorial i • (1 - X) ^ (n - i)

theorem Polynomial.differentiableAt_inv_special {x a : ℝ} {n : ℕ} (ha : a > 0) (hx : 1 - a * x = 0) : ¬DifferentiableAt ℝ (fun (x : ℝ) => ↑n.factorial * a ^ n / (1 - a * x) ^ (n + 1)) x

theorem Polynomial.n_derivative {a : ℝ} (n : ℕ) (ha : a > 0) : (deriv^[n] fun (x : ℝ) => 1 / (1 - a * x)) = fun (x : ℝ) => ↑n.factorial * a ^ n / (1 - a * x) ^ (n + 1)

theorem Polynomial.differentiableAt_inv_special' (c x y z : ℝ) (n : ℕ) (hc : c ≠ 0) (hx : x ∈ Set.Ioo 0 1) (hz : z ∈ Set.Ioo 0 1) (h1 : 1 - (1 - x * y) * z = 0) : ¬DifferentiableAt ℝ (fun (y : ℝ) => c / (1 - (1 - x * y) * z) ^ (n + 1)) y

theorem Polynomial.n_derivative' {x z : ℝ} (n : ℕ) (hx : x ∈ Set.Ioo 0 1) (hz : z ∈ Set.Ioo 0 1) : (deriv^[n] fun (y : ℝ) => 1 / (1 - (1 - x * y) * z)) = fun (y : ℝ) => (-1) ^ n * ↑n.factorial * (x * z) ^ n / (1 - (1 - x * y) * z) ^ (n + 1)

theorem Polynomial.shiftedLegendre_poly_eval_zero_eq_zero {n m : ℕ} (h : m < n) : eval 0 ((⇑derivative)^[m] (X ^ n * (1 - X) ^ n)) = 0

theorem Polynomial.shiftedLegendre_poly_eval_one_eq_zero {n m : ℕ} (h : m < n) : eval 1 ((⇑derivative)^[m] (X ^ n * (1 - X) ^ n)) = 0

theorem Polynomial.shiftedLegendre_continuousOn {n m : ℕ} : ContinuousOn (fun (x : ℝ) => eval x ((⇑derivative)^[n - m] (X ^ n * (1 - X) ^ n))) (Set.uIcc 0 1)

theorem Polynomial.special_deriv_div_continuousOn {m : ℕ} {x z : ℝ} (hx : x ∈ Set.Ioo 0 1) (hz : z ∈ Set.Ioo 0 1) : ContinuousOn (fun (u : ℝ) => deriv^[m] (fun (y : ℝ) => 1 / (1 - (1 - x * y) * z)) u) (Set.uIcc 0 1)

theorem Polynomial.integral_shiftedLegendre_mul_smooth_eq_aux {x z : ℝ} (n m : ℕ) (h : m ≤ n) (hx : x ∈ Set.Ioo 0 1) (hz : z ∈ Set.Ioo 0 1) : ∫ (y : ℝ) in 0..1, eval y ((⇑derivative)^[n] (X ^ n * (1 - X) ^ n)) * (fun (y : ℝ) => 1 / (1 - (1 - x * y) * z)) y = (-1) ^ m * ∫ (y : ℝ) in 0..1, eval y ((⇑derivative)^[n - m] (X ^ n * (1 - X) ^ n)) * deriv^[m] (fun (y : ℝ) => 1 / (1 - (1 - x * y) * z)) y

theorem Polynomial.integral_legendre_mul_smooth_eq {x z : ℝ} (n : ℕ) (hx : x ∈ Set.Ioo 0 1) (hz : z ∈ Set.Ioo 0 1) : ∫ (y : ℝ) in 0..1, eval y (shiftedLegendre n) * (fun (y : ℝ) => 1 / (1 - (1 - x * y) * z)) y = (-1) ^ n / ↑n.factorial * ∫ (y : ℝ) in 0..1, y ^ n * (1 - y) ^ n * deriv^[n] (fun (y : ℝ) => 1 / (1 - (1 - x * y) * z)) y

theorem Polynomial.legendre_integral_special {x z : ℝ} (n : ℕ) (hx : x ∈ Set.Ioo 0 1) (hz : z ∈ Set.Ioo 0 1) : ∫ (y : ℝ) in 0..1, eval y (shiftedLegendre n) * (1 / (1 - (1 - x * y) * z)) = ∫ (y : ℝ) in 0..1, (x * y * z) ^ n * (1 - y) ^ n / (1 - (1 - x * y) * z) ^ (n + 1)