Research proof index

The eigenfunctions are square integrable.

If f is a function ℝ → ℂ satisfying MemHS f such that it is orthogonal to all eigenfunction n then the fourier transform of f (x) * e ^ (- x ^ 2 / (2 ξ^2)) is zero. The proof of this result relies on orthogonal_exp_of_mem_orthogonal.

If f is a function ℝ → ℂ satisfying MemHS f such that it is orthogonal to all eigenfunction n then it is orthogonal to e ^ (I c x) * e ^ (- x ^ 2 / (2 ξ^2)) for any real c. The proof of this result relies on the expansion of e ^ (I c x) in terms of x^r/r! and using orthogonal_power_of_mem_orthogonal along with integrability conditions.

If f is a function ℝ → ℂ satisfying MemHS f such that it is orthogonal to all eigenfunction n then it is orthogonal to x ^ r * e ^ (- x ^ 2 / (2 ξ^2)) the proof of this result relies on the fact that Hermite polynomials span polynomials.

The nth eigenfunction satisfies the time-independent Schrodinger equation with respect to the nth eigenvalue. That is to say for Q a harmonic oscillator, Q.schrodingerOperator (Q.eigenfunction n) x = Q.eigenValue n * Q.eigenfunction n x. The proof of this result is done by explicit calculation of derivatives.

A function f satisfies MemHS f if and only if it is almost everywhere strongly measurable, and square integrable.