Legendre polynomials

Stream: Is there code for X?

[Junqi Liu]

How to define a class of polynomials like P_n(x) = n * x? For any n : N, P_n(x) will be an certain polynomial.

[Adam Topaz]

you can do something like this:

import Mathlib.Data.Polynomial.Basic

noncomputable
example (n : ℕ) (R : Type*) [Semiring R] : Polynomial R :=
  n * .X

[Junqi Liu]

Thank you so much! But I want to ask you that what is the mean of Semiring R here? And if I want to define  P_n(x) = (1 / x)^(n) which means the n-th derivative of 1 / x, what should I do?

[Yury G. Kudryashov]

deriv^[n] (fun x => 1 / x). Not tested. Clearly, this is not a polynomial.

[Junqi Liu]

Yury G. Kudryashov said:

deriv^[n] (fun x => 1 / x). Not tested. Clearly, this is not a polynomial.

yeah! I konw. Actually I want to define Legendre Polynomial which is a polynomial. haha! Thanks so much!

[Junqi Liu]

Yury G. Kudryashov said:

deriv^[n] (fun x => 1 / x). Not tested. Clearly, this is not a polynomial.

I find it doesn't work very well, can you help me define a set of legendre polynomials?

[Notification Bot]

This topic was moved here from #lean4 > define polynomial by Yury G. Kudryashov.

[Yury G. Kudryashov]

You can use

import Mathlib

open scoped Nat

namespace Polynomial

noncomputable def legendre (n : ℕ) : ℝ[X] :=
  C (1 / (2^n * n !) : ℝ) * derivative^[n] ((X ^ 2 - 1) ^ n)

noncomputable def legendre' (n : ℕ) : ℝ[X] :=
  (1 / (2^n) : ℝ) •
    ∑ k in Finset.range (n + 1), (Nat.choose n k) ^ 2 • (X - 1) ^ (n - k) * (X + 1) ^ k

end Polynomial

[Yury G. Kudryashov]

If you're going to contribute it to Mathlib, then there is a design choice:

• define it as real polynomials, use aeval to evaluate at complex numbers;
• take {K : Type*} [ROrCLike K] as an argument;
• define it over any field;
• define a non-normed version (the numerator, or the numerator divided by $n!$, it's still a polynomial with integer coefficients, see primed definition) over any ring, then define the normed version over any field.

I don't know if Legendre polynomials over fields other than $\mathbb{R}$ or $\mathbb{C}$ are useful.

[Mitchell Lee]

They are useful

[Mitchell Lee]

I like the fourth choice the most, and you can do it for any $\mathbb{Q}$-algebra (or more generally, any ring in which 2 is invertible)

[Junqi Liu]

nice! Thanks, it's very helpful to me!

[Antoine Chambert-Loir]

Replacing the interval $[-1;1]$ by the interval $[0;1]$, and the polynomial $T^2-1$ by $T(T-1)$, one gets the shifted Legendre polynomials which have better integrality properties.