Research proof index

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.