hermite polynomials

Stream: maths

[Alex Ghorbani]

Hi all! I'm currently working on writing up a file on Hermite polynomials and I had a quick question regarding coefficients for polynomials. Namely, is there a way to require that the coefficients of a polynomials be in ℝ?

I was looking at the existing code for Chebyshev and Bernstein polynomials and this does not seem to be an issue because those can be generalized to have coefficients in arbitrary commutative rings. Since Hermite polynomials use the exponential function, I'm not quite sure how one would even go about generalizing it or whatever, but for now I feel like just restricting the coefficients would suffice.

Thanks!

[Damiano Testa]

Using f : ℝ[X] gives you a polynomial with real coefficients. Is this what you had in mind?

[Damiano Testa]

(I'm assuming you have the right imports and open_locales available)

[Damiano Testa]

Here is a working example:

import data.polynomial.basic
import analysis.special_functions.trigonometric.bounds

open polynomial
open_locale polynomial real

variables (f : ℝ[X]) (a : ℕ)
#check f.coeff a
-- f.coeff a : ℝ

#check C (π ^ real.pi) * X + C (2 ^ (real.exp 1))
-- ⇑C (π ^ π) * X + ⇑C (2 ^ real.exp 1) : ℝ[X]

[Alex Ghorbani]

Yes, you are right. My apologies, I meant to ask about the X. Like my problem is that in the definition of Hermite polynomials, you have to take e^X but I guess we don't always know if we can take the exponential. Does this make more sense?

[Damiano Testa]

The X in polynomials is a variable. Taking e ^ X does not give a polynomial. It seems that you either want (formal) power series (unlikely), or define a custom "truncated exponential" (more likely).

[Damiano Testa]

Saying it in a different way: there is no exponential function on reals that takes a polynomial and returns a polynomial. This is how Lean would interpret e ^ X.

[Alex Ghorbani]

Ok, I see what you're saying. This is the definition I'm trying to implement:
H_n(x) ≔ (−1)^n exp(1/2 * x^2) d/dx^n exp(−1/2 * x^2)
This should be a polynomial in x, right?

[Yaël Dillies]

Yes, but that it is a polynomial requires a proof. It's not structurally a polynomial.

[Alex Ghorbani]

oooh, thank you that makes sense

[Damiano Testa]

I agree with Yaël: what you gave is the definition of a formal power series that happens to have only finitely many non-zero coefficients.

[Alex Ghorbani]

ok so I will define this function and then I will prove it is a polynomial

[Damiano Testa]

I think that it will be easier to give a definition that is "directly" a polynomial and then develop some API to prove that it satisfies the identity that you stated.

[Yaël Dillies]

Sniped :sweat_smile:

[Damiano Testa]

Actually, I was typing my comment before Alex's response! :smile:

[Yaël Dillies]

And you sent it before mine that was about to say the exact same thing.

[Alex Ghorbani]

Thank you both for your help! I will probably resume this tomorrow morning

[Eric Wieser]

I would guess docs#exp is not relevant here because polynomial exponentials don't converge in general, even if there is a sensible topology or norm somewhere

[Kevin Buzzard]

I think the thing to do would be to use a more Lean-appropriate definition of Hermite polynomials (for example $(x-d/dx)^n 1$ or $\sum_{m\leq n/2}(-1)^{m}n!x^{n-2m}/(m!(n-2m)!)$ and then prove that this equals the definition involving exp, formalised as an equality of elements of $\mathbb{Q}[[x]]$, the power series ring.

[Kevin Buzzard]

I guess another approach would be to formalise Generalized Laguerre polynomials (which have a simple recursive definition) and then use the fact that Hermite polynomials are essentially the special case $\alpha=-1/2$.

[Junyan Xu]

It seems the correct abstraction here is differential field, where you can formally adjoin an exponential function:

The differential field ℚ(t) fails to have a solution to the differential equation ∂(u)=u, but expands to a larger differential field including the function e^t which does have a solution to this equation [of course ℚ((t)) is such a field].