PhyslibSearch

Physlib.Mathematics.SpecialFunctions.PhysHermite

48 declarations

definition

Physicists Hermite polynomials Hn(x)H_n(x)

#physHermite

The physicist's Hermite polynomials Hn(x)H_n(x) are a sequence of polynomials with integer coefficients (elements of Z[x]\mathbb{Z}[x]) defined recursively for nNn \in \mathbb{N} by the base case \[ H_0(x) = 1 \] and the recurrence relation \[ H_{n+1}(x) = 2x H_n(x) - \frac{d}{dx} H_n(x) \] where xx represents the indeterminate and ddx\frac{d}{dx} denotes the polynomial derivative.

theorem

Recurrence Relation for Hn+1(x)H_{n+1}(x)

#physHermite_succ

For any natural number nn, the physicist's Hermite polynomial Hn+1(x)H_{n+1}(x) satisfies the recurrence relation \[ H_{n+1}(x) = 2x H_n(x) - \frac{d}{dx} H_n(x) \] where Hn(x)H_n(x) denotes the nn-th physicist's Hermite polynomial and ddx\frac{d}{dx} denotes the polynomial derivative.

theorem

Iterative definition of physicist's Hermite polynomials Hn(x)=(2xddx)n(1)H_n(x) = (2x - \frac{d}{dx})^n (1)

#physHermite_eq_iterate

For any natural number nn, the nn-th physicist's Hermite polynomial Hn(x)H_n(x) is equal to the nn-fold iteration of the operator p(x)2xp(x)ddxp(x)p(x) \mapsto 2xp(x) - \frac{d}{dx}p(x) applied to the constant polynomial 11. That is, \[ H_n(x) = \left( 2x - \frac{d}{dx} \right)^n (1) \] where xx represents the indeterminate and ddx\frac{d}{dx} denotes the polynomial derivative.

theorem

H0(x)=1H_0(x) = 1

#physHermite_zero

The 0th physicist's Hermite polynomial H0(x)H_0(x) is equal to the constant polynomial 11. That is, H0(x)=1H_0(x) = 1.

theorem

H1(x)=2xH_1(x) = 2x

#physHermite_one

The first physicist's Hermite polynomial H1(x)H_1(x) is equal to 2x2x, where xx represents the indeterminate.

theorem

ddxHn+1(x)=2(n+1)Hn(x)\frac{d}{dx} H_{n+1}(x) = 2(n+1) H_n(x)

#derivative_physHermite_succ

For any natural number nn, the derivative of the (n+1)(n+1)-th physicist's Hermite polynomial Hn+1(x)H_{n+1}(x) is equal to 2(n+1)Hn(x)2(n+1) H_n(x). That is, \[ \frac{d}{dx} H_{n+1}(x) = 2(n+1) H_n(x). \]

theorem

ddxHn(x)=2nHn1(x)\frac{d}{dx} H_n(x) = 2n H_{n-1}(x)

#derivative_physHermite

For any natural number nn, let Hn(x)H_n(x) denote the nn-th physicist's Hermite polynomial. The derivative of Hn(x)H_n(x) with respect to xx is given by \[ \frac{d}{dx} H_n(x) = 2n H_{n-1}(x), \] where n1n-1 is defined to be 00 if n=0n=0.

theorem

Hn+1(x)=2xHn(x)2nHn1(x)H_{n+1}(x) = 2x H_n(x) - 2n H_{n-1}(x)

#physHermite_succ'

For any natural number nn, let Hn(x)H_n(x) denote the nn-th physicist's Hermite polynomial. The sequence of polynomials satisfies the three-term recurrence relation: \[ H_{n+1}(x) = 2x H_n(x) - 2n H_{n-1}(x) \] where n1n-1 is defined to be 00 if n=0n=0.

theorem

[x0]Hn+1(x)=[x1]Hn(x)[x^0] H_{n+1}(x) = -[x^1] H_n(x)

#coeff_physHhermite_succ_zero

For any natural number nn, let Hn(x)H_n(x) denote the nn-th physicist's Hermite polynomial. The constant term (the coefficient of x0x^0) of Hn+1(x)H_{n+1}(x) is equal to the negative of the coefficient of x1x^1 in Hn(x)H_n(x). This can be expressed as \[ [x^0] H_{n+1}(x) = -[x^1] H_n(x) \] where [xk]P(x)[x^k] P(x) denotes the coefficient of the kk-th power of the indeterminate xx in the polynomial P(x)P(x).

theorem

Recurrence relation for coefficients [xk+1]Hn+1(x)[x^{k+1}] H_{n+1}(x)

#coeff_physHermite_succ_succ

For any natural numbers nn and kk, let Hn(x)H_n(x) denote the nn-th physicist's Hermite polynomial. The coefficient of xk+1x^{k+1} in the polynomial Hn+1(x)H_{n+1}(x) is given by the relation \[ [x^{k+1}] H_{n+1}(x) = 2 [x^k] H_n(x) - (k+2) [x^{k+2}] H_n(x) \] where [xm]P(x)[x^m] P(x) denotes the coefficient of the mm-th power of the indeterminate xx in the polynomial P(x)P(x).

theorem

[xk]Hn(x)=0[x^k] H_n(x) = 0 for n<kn < k

#coeff_physHermite_of_lt

For any natural numbers nn and kk such that n<kn < k, let Hn(x)H_n(x) denote the nn-th physicist's Hermite polynomial. The coefficient of xkx^k in the polynomial Hn(x)H_n(x) is zero. This can be expressed as \[ [x^k] H_n(x) = 0 \] where [xk]P(x)[x^k] P(x) denotes the coefficient of the kk-th power of the indeterminate xx in the polynomial P(x)P(x).

theorem

[xn]Hn(x)=2n[x^n] H_n(x) = 2^n

#coeff_physHermite_self_succ

For any natural number nn, let Hn(x)H_n(x) denote the nn-th physicist's Hermite polynomial. The coefficient of the xnx^n term in Hn(x)H_n(x) is 2n2^n. This can be expressed as \[ [x^n] H_n(x) = 2^n \] where [xn]P(x)[x^n] P(x) denotes the coefficient of the nn-th power of the indeterminate xx in the polynomial P(x)P(x).

theorem

deg(Hn(x))=n\deg(H_n(x)) = n

#degree_physHermite

For any natural number nn, let Hn(x)H_n(x) denote the nn-th physicist's Hermite polynomial. The degree of the polynomial Hn(x)H_n(x) is equal to nn. This can be expressed as \[ \deg(H_n(x)) = n \] where deg(P)\deg(P) denotes the degree of the polynomial PP.

theorem

natDegree(Hn(x))=n\text{natDegree}(H_n(x)) = n

#natDegree_physHermite

For any natural number nn, let Hn(x)H_n(x) denote the nn-th physicist's Hermite polynomial. The natural degree of the polynomial Hn(x)H_n(x) is equal to nn. This can be expressed as: \[ \text{natDegree}(H_n(x)) = n \] where natDegree(P)\text{natDegree}(P) denotes the degree of the polynomial PP as a natural number.

theorem

dmdxmHn(x)=0\frac{d^m}{dx^m} H_n(x) = 0 for m>nm > n

#iterate_derivative_physHermite_of_gt

Let Hn(x)H_n(x) denote the nn-th physicist's Hermite polynomial. For any natural numbers nn and mm such that n<mn < m, the mm-th derivative of Hn(x)H_n(x) is equal to zero. This is expressed as: \[ \frac{d^m}{dx^m} H_n(x) = 0 \] where dmdxm\frac{d^m}{dx^m} denotes the mm-th order derivative with respect to xx.

theorem

dndxnHn(x)=n!2n\frac{d^n}{dx^n} H_n(x) = n! 2^n

#iterate_derivative_physHermite_self

For any natural number nn, let Hn(x)H_n(x) denote the nn-th physicist's Hermite polynomial. The nn-th derivative of Hn(x)H_n(x) is the constant polynomial n!2nn! \cdot 2^n. This is expressed as: \[ \frac{d^n}{dx^n} H_n(x) = n! \cdot 2^n \] where n!n! denotes the factorial of nn.

theorem

Leading coefficient of Hn(x)=2nH_n(x) = 2^n

#physHermite_leadingCoeff

For any natural number nn, let Hn(x)H_n(x) denote the nn-th physicist's Hermite polynomial. The leading coefficient of Hn(x)H_n(x) is 2n2^n.

theorem

Hn(x)0H_n(x) \neq 0

#physHermite_ne_zero

For any natural number nNn \in \mathbb{N}, the nn-th physicist's Hermite polynomial Hn(x)H_n(x) is not the zero polynomial.

instance

Coercion from Z[x]\mathbb{Z}[x] to functions RR\mathbb{R} \to \mathbb{R}

#instCoeFunPolynomialIntForallReal_physlib

This instance allows a polynomial pZ[x]p \in \mathbb{Z}[x] with integer coefficients to be treated as a function from the real numbers to the real numbers, mapping xRx \in \mathbb{R} to the evaluation of the polynomial at that point, p(x)p(x).

theorem

Hn(x)H_n(x) equals its algebraic evaluation at xx

#physHermite_eq_aeval

For any natural number nNn \in \mathbb{N} and any real number xRx \in \mathbb{R}, the value of the nn-th physicist's Hermite polynomial HnH_n evaluated at xx is equal to its algebraic evaluation at xx: \[ H_n(x) = \operatorname{aeval}_x(H_n) \] where Hn(x)H_n(x) denotes the polynomial HnZ[x]H_n \in \mathbb{Z}[x] viewed as a function from R\mathbb{R} to R\mathbb{R} via coercion, and aevalx\operatorname{aeval}_x denotes the algebraic evaluation of the polynomial at the point xx.

theorem

H0(x)=1H_0(x) = 1

#physHermite_zero_apply

For any real number xx, the zeroth physicist's Hermite polynomial evaluated at xx is equal to 11, denoted as H0(x)=1H_0(x) = 1.

theorem

(Hn(x))m=(Hnm)(x)(H_n(x))^m = (H_n^m)(x)

#physHermite_pow

For any natural numbers n,mNn, m \in \mathbb{N} and any real number xRx \in \mathbb{R}, let HnH_n be the nn-th physicist's Hermite polynomial. Then the mm-th power of the value of HnH_n at xx is equal to the evaluation of the polynomial HnmH_n^m at xx: \[ (H_n(x))^m = (H_n^m)(x) \]

theorem

Hn+1(x)=2xHn(x)2nHn1(x)H_{n+1}(x) = 2x H_n(x) - 2n H_{n-1}(x) for Real Functions

#physHermite_succ_fun

For any natural number nn, the nn-th physicist's Hermite polynomial HnH_n, when viewed as a function from the real numbers R\mathbb{R} to R\mathbb{R}, satisfies the three-term recurrence relation: \[ H_{n+1}(x) = 2x H_n(x) - 2n H_{n-1}(x) \] where n1n-1 is defined to be 00 if n=0n=0.

theorem

Hn+1(x)=2xHn(x)2nHn1(x)H_{n+1}(x) = 2x H_n(x) - 2n H_{n-1}(x)

#physHermite_succ_fun'

For any natural number nn, let Hn(x)H_n(x) denote the nn-th physicist's Hermite polynomial evaluated at xRx \in \mathbb{R}. The sequence of functions satisfies the recurrence relation: \[ H_{n+1}(x) = 2x H_n(x) - 2n H_{n-1}(x) \] where n1n-1 is defined to be 00 if n=0n=0.

theorem

The mm-th Iterated Derivative of HnH_n Equals its mm-th Formal Polynomial Derivative Evaluation

#iterated_deriv_physHermite_eq_aeval

For any natural numbers nn and mm, the mm-th iterated derivative of the nn-th physicist's Hermite polynomial HnH_n (viewed as a function) is equal to the evaluation of its mm-th formal polynomial derivative. That is, \[ \frac{d^m}{dx^m} H_n(x) = (H_n^{(m)})(x) \] where Hn(m)H_n^{(m)} denotes the mm-th formal derivative of the polynomial HnH_n.

theorem

Physicists Hermite polynomial HnH_n is differentiable at xx

#physHermite_differentiableAt

For any natural number nn and any real number xx, the nn-th physicist's Hermite polynomial HnH_n is differentiable at xx.

theorem

The mm-th Derivative of HnH_n is Differentiable at xx

#deriv_physHermite_differentiableAt

Let HnH_n denote the nn-th physicist's Hermite polynomial. For any natural numbers nn and mm, the mm-th iterated derivative of HnH_n, denoted by dmdxmHn\frac{d^m}{dx^m} H_n, is differentiable at any point xRx \in \mathbb{R}.

theorem

ddxHn(x)=2nHn1(x)\frac{d}{dx} H_n(x) = 2n H_{n-1}(x)

#deriv_physHermite

For any natural number nn, let Hn(x)H_n(x) denote the nn-th physicist's Hermite polynomial. The derivative of HnH_n (as a function from R\mathbb{R} to R\mathbb{R}) is given by \[ \frac{d}{dx} H_n(x) = 2n H_{n-1}(x), \] where n1n-1 is defined to be 00 if n=0n=0.

theorem

D(Hnf)(x)=2nHn1(f(x))Df(x)D(H_n \circ f)(x) = 2n H_{n-1}(f(x)) \cdot Df(x)

#fderiv_physHermite

Let EE be a normed real vector space, xEx \in E, and f:ERf: E \to \mathbb{R} be a function that is differentiable at xx. For any natural number nn, let HnH_n denote the nn-th physicist's Hermite polynomial. The Fréchet derivative of the composition HnfH_n \circ f at xx is given by \[ D(H_n \circ f)(x) = 2n H_{n-1}(f(x)) \cdot Df(x), \] where Df(x)Df(x) is the Fréchet derivative of ff at xx, and n1n-1 is defined to be 00 if n=0n=0.

theorem

ddxHn(f(x))=2nHn1(f(x))f(x)\frac{d}{dx} H_n(f(x)) = 2n H_{n-1}(f(x)) f'(x)

#deriv_physHermite'

Let xx be a real number and f:RRf: \mathbb{R} \to \mathbb{R} be a function that is differentiable at xx. For any natural number nn, let HnH_n denote the nn-th physicist's Hermite polynomial. The derivative of the composition HnfH_n \circ f evaluated at xx is given by \[ \frac{d}{dx} H_n(f(x)) = 2n H_{n-1}(f(x)) f'(x), \] where f(x)f'(x) is the derivative of ff at xx, and n1n-1 is defined to be 00 if n=0n=0.

theorem

Hn(x)=(1)nHn(x)H_n(-x) = (-1)^n H_n(x)

#physHermite_parity

For any natural number nn and any real number xx, the nn-th physicist's Hermite polynomial HnH_n satisfies the parity relation: \[ H_n(-x) = (-1)^n H_n(x) \]

theorem

dndxnex2=(1)nHn(x)ex2\frac{d^n}{dx^n} e^{-x^2} = (-1)^n H_n(x) e^{-x^2}

#deriv_gaussian_eq_physHermite_mul_gaussian

For any natural number nn and any real number xx, the nn-th derivative of the Gaussian function ex2e^{-x^2} evaluated at xx is given by \[ \frac{d^n}{dx^n} e^{-x^2} = (-1)^n H_n(x) e^{-x^2}, \] where Hn(x)H_n(x) denotes the nn-th physicist's Hermite polynomial.

theorem

Hn(x)=(1)n(dndxnex2)/ex2H_n(x) = (-1)^n \left( \frac{d^n}{dx^n} e^{-x^2} \right) / e^{-x^2}

#physHermite_eq_deriv_gaussian

For any natural number nn and any real number xx, the nn-th physicist's Hermite polynomial Hn(x)H_n(x) is given by \[ H_n(x) = (-1)^n \frac{\frac{d^n}{dx^n} e^{-x^2}}{e^{-x^2}}, \] where dndxn\frac{d^n}{dx^n} denotes the nn-th derivative.

theorem

Hn(x)=(1)n(dndxnex2)ex2H_n(x) = (-1)^n \left( \frac{d^n}{dx^n} e^{-x^2} \right) e^{x^2}

#physHermite_eq_deriv_gaussian'

For any natural number nn and any real number xx, the nn-th physicist's Hermite polynomial Hn(x)H_n(x) is given by the formula \[ H_n(x) = (-1)^n \left( \frac{d^n}{dx^n} e^{-x^2} \right) e^{x^2}, \] where dndxn\frac{d^n}{dx^n} denotes the nn-th derivative with respect to xx.

theorem

Integrability of P(x)ebx2P(x) e^{-bx^2} for b>0b > 0

#guassian_integrable_polynomial

Let bRb \in \mathbb{R} be a positive real number (b>0b > 0), and let PZ[x]P \in \mathbb{Z}[x] be a polynomial with integer coefficients. Then the function xP(x)ebx2x \mapsto P(x) e^{-bx^2} is integrable over the real line R\mathbb{R} with respect to the Lebesgue measure.

theorem

Integrability of P(cx)ebx2P(cx) e^{-bx^2} for b>0b > 0

#guassian_integrable_polynomial_cons

Let bb and cc be real numbers such that b>0b > 0, and let PP be a polynomial with integer coefficients. Then the function f(x)=P(cx)ebx2f(x) = P(cx) e^{-bx^2} is integrable on R\mathbb{R} with respect to the Lebesgue measure.

theorem

Integrability of dmdxmHp(x)dndxnex2\frac{d^m}{dx^m} H_p(x) \cdot \frac{d^n}{dx^n} e^{-x^2}

#physHermite_gaussian_integrable

For any natural numbers n,p,n, p, and mm, the product of the mm-th derivative of the pp-th physicist's Hermite polynomial Hp(x)H_p(x) and the nn-th derivative of the Gaussian function ex2e^{-x^2} is integrable over the real line R\mathbb{R} with respect to the Lebesgue measure. That is, the function \[ f(x) = \left( \frac{d^m}{dx^m} H_p(x) \right) \left( \frac{d^n}{dx^n} e^{-x^2} \right) \] is integrable.

theorem

HnHmex2dx=(1)mHndmdxmex2dx\int H_n H_m e^{-x^2} dx = (-1)^m \int H_n \frac{d^m}{dx^m} e^{-x^2} dx

#integral_physHermite_mul_physHermite_eq_integral_deriv_exp

For any natural numbers nn and mm, the integral over the real line of the product of the nn-th and mm-th physicist's Hermite polynomials, Hn(x)H_n(x) and Hm(x)H_m(x), weighted by the Gaussian function ex2e^{-x^2}, satisfies the identity: \[ \int_{-\infty}^{\infty} H_n(x) H_m(x) e^{-x^2} \, dx = (-1)^m \int_{-\infty}^{\infty} H_n(x) \frac{d^m}{dx^m} (e^{-x^2}) \, dx \] where dmdxm\frac{d^m}{dx^m} denotes the mm-th derivative with respect to xx.

theorem

HnHmex2dx=(1)mpdpdxpHndmpdxmpex2dx\int H_n H_m e^{-x^2} dx = (-1)^{m-p} \int \frac{d^p}{dx^p} H_n \frac{d^{m-p}}{dx^{m-p}} e^{-x^2} dx

#integral_physHermite_mul_physHermite_eq_integral_deriv_inductive

For any natural numbers nn and mm, and for any natural number pp such that pmp \leq m, the integral over the real line of the product of the nn-th and mm-th physicist's Hermite polynomials Hn(x)H_n(x) and Hm(x)H_m(x) weighted by the Gaussian function ex2e^{-x^2} satisfies the identity: \[ \int_{-\infty}^{\infty} H_n(x) H_m(x) e^{-x^2} \, dx = (-1)^{m-p} \int_{-\infty}^{\infty} \left( \frac{d^p}{dx^p} H_n(x) \right) \left( \frac{d^{m-p}}{dx^{m-p}} e^{-x^2} \right) \, dx \] where dkdxk\frac{d^k}{dx^k} denotes the kk-th iterated derivative with respect to xx.

theorem

HnHmex2dx=(dmdxmHn)ex2dx\int H_n H_m e^{-x^2} dx = \int \left( \frac{d^m}{dx^m} H_n \right) e^{-x^2} dx

#integral_physHermite_mul_physHermite_eq_integral_deriv

For any natural numbers nn and mm, the integral over the real line of the product of the nn-th and mm-th physicist's Hermite polynomials Hn(x)H_n(x) and Hm(x)H_m(x) weighted by the Gaussian function ex2e^{-x^2} is equal to the integral of the mm-th derivative of Hn(x)H_n(x) weighted by the same Gaussian function: \[ \int_{-\infty}^{\infty} H_n(x) H_m(x) e^{-x^2} \, dx = \int_{-\infty}^{\infty} \left( \frac{d^m}{dx^m} H_n(x) \right) e^{-x^2} \, dx \] where dmdxm\frac{d^m}{dx^m} denotes the mm-th iterated derivative with respect to xx.

theorem

HnHmex2dx=0\int H_n H_m e^{-x^2} dx = 0 for n<mn < m

#physHermite_orthogonal_lt

Let Hn(x)H_n(x) denote the nn-th physicist's Hermite polynomial. For any natural numbers nn and mm such that n<mn < m, the integral over the real line of the product of Hn(x)H_n(x) and Hm(x)H_m(x) weighted by the Gaussian function ex2e^{-x^2} is zero: \[ \int_{-\infty}^{\infty} H_n(x) H_m(x) e^{-x^2} \, dx = 0 \]

theorem

Orthogonality of Physicist's Hermite Polynomials: HnHmex2dx=0\int H_n H_m e^{-x^2} dx = 0 for nmn \neq m

#physHermite_orthogonal

Let Hn(x)H_n(x) denote the nn-th physicist's Hermite polynomial. For any natural numbers nn and mm such that nmn \neq m, the integral over the real line of the product of Hn(x)H_n(x) and Hm(x)H_m(x) weighted by the Gaussian function ex2e^{-x^2} is zero: \[ \int_{-\infty}^{\infty} H_n(x) H_m(x) e^{-x^2} \, dx = 0 \]

theorem

Orthogonality of Scaled Physicist's Hermite Polynomials: Hn(cx)Hm(cx)ec2x2dx=0\int H_n(cx) H_m(cx) e^{-c^2 x^2} dx = 0 for nmn \neq m

#physHermite_orthogonal_cons

Let Hn(x)H_n(x) denote the nn-th physicist's Hermite polynomial. For any natural numbers nn and mm such that nmn \neq m, and for any real number cc, the integral over the real line of the product of Hn(cx)H_n(cx) and Hm(cx)H_m(cx) weighted by the Gaussian function ec2x2e^{-c^2 x^2} is zero: \[ \int_{-\infty}^{\infty} H_n(cx) H_m(cx) e^{-c^2 x^2} \, dx = 0 \]

theorem

Hn2ex2dx=n!2nπ\int H_n^2 e^{-x^2} dx = n! 2^n \sqrt{\pi}

#physHermite_norm

For any natural number nn, the integral over the real line of the square of the nn-th physicist's Hermite polynomial Hn(x)H_n(x) weighted by the Gaussian function ex2e^{-x^2} is given by: \[ \int_{-\infty}^{\infty} (H_n(x))^2 e^{-x^2} \, dx = n! 2^n \sqrt{\pi} \] where Hn(x)H_n(x) denotes the nn-th physicist's Hermite polynomial.

theorem

Hn(cx)2ec2x2dx=c1n!2nπ\int H_n(cx)^2 e^{-c^2 x^2} dx = |c^{-1}| n! 2^n \sqrt{\pi}

#physHermite_norm_cons

For any natural number nn and any real number cc, the integral over the real line of the square of the nn-th physicist's Hermite polynomial HnH_n evaluated at cxcx, weighted by the Gaussian function ec2x2e^{-c^2 x^2}, is given by: \[ \int_{-\infty}^{\infty} (H_n(cx))^2 e^{-c^2 x^2} \, dx = \left| \frac{1}{c} \right| n! 2^n \sqrt{\pi} \] where HnH_n denotes the nn-th physicist's Hermite polynomial.

theorem

PZ[x]P \in \mathbb{Z}[x] with deg(P)=n\deg(P) = n is in the R\mathbb{R}-span of {Hk}\{H_k\}

#polynomial_mem_physHermite_span_induction

Let Hk(x)H_k(x) denote the kk-th physicist's Hermite polynomial. For any polynomial PP with integer coefficients (i.e., PZ[x]P \in \mathbb{Z}[x]) and any natural number nn such that the degree of PP is equal to nn, the function P:RRP: \mathbb{R} \to \mathbb{R} belongs to the R\mathbb{R}-linear span of the set of all physicist's Hermite polynomials {Hk:kN}\{H_k : k \in \mathbb{N}\}.

theorem

PZ[x]P \in \mathbb{Z}[x] is in the R\mathbb{R}-span of physicist's Hermite polynomials {Hn}\{H_n\}

#polynomial_mem_physHermite_span

Let Hn(x)H_n(x) denote the nn-th physicist's Hermite polynomial. For any polynomial PP with integer coefficients (i.e., PZ[x]P \in \mathbb{Z}[x]), the function P:RRP : \mathbb{R} \to \mathbb{R} belongs to the R\mathbb{R}-linear span of the set of all physicist's Hermite polynomials {Hn:nN}\{H_n : n \in \mathbb{N}\}.

theorem

cos(cx)\cos(cx) is in the topological closure of the R\mathbb{R}-span of physicist's Hermite polynomials

#cos_mem_physHermite_span_topologicalClosure

Let Hn(x)H_n(x) denote the nn-th physicist's Hermite polynomial. For any real constant cRc \in \mathbb{R}, the function f(x)=cos(cx)f(x) = \cos(cx) belongs to the topological closure of the R\mathbb{R}-linear span of the set of all physicist's Hermite polynomials {Hn:nN}\{H_n : n \in \mathbb{N}\}.