noncomputable def GaussianSpace.ornsteinUhlenbeckOp1D (ρ : ℝ) (f : ℝ → ℝ) (x : ℝ) : ℝ

noncomputable def GaussianSpace.ornsteinUhlenbeckOp {n : ℕ} (ρ : ℝ) (f : EuclideanSpace ℝ (Fin n) → ℝ) (x : EuclideanSpace ℝ (Fin n)) : ℝ

noncomputable def GaussianSpace.stdGaussianDensity (t : ℝ) : ℝ

theorem GaussianSpace.stdGaussianDensity_eq_gaussianPDFReal (t : ℝ) : stdGaussianDensity t = ProbabilityTheory.gaussianPDFReal 0 1 t

theorem GaussianSpace.integral_stdGaussianDensity_eq_one : ∫ (t : ℝ), stdGaussianDensity t = 1

noncomputable def GaussianSpace.hermiteFun (k : ℕ) (x : ℝ) : ℝ

noncomputable def GaussianSpace.hermiteFun1 (k : ℕ) (x : EuclideanSpace ℝ (Fin 1)) : ℝ

theorem GaussianSpace.ornsteinUhlenbeck_hermite_1D (k : ℕ) (ρ : ℝ) (hρ : ρ ∈ Set.Icc (-1) 1) (x : ℝ) : ornsteinUhlenbeckOp1D ρ (hermiteFun k) x = ρ ^ k * hermiteFun k x

theorem GaussianSpace.ornsteinUhlenbeck_hermite (k : ℕ) (ρ : ℝ) (hρ : ρ ∈ Set.Icc (-1) 1) (x : EuclideanSpace ℝ (Fin 1)) : ornsteinUhlenbeckOp ρ (hermiteFun1 k) x = ρ ^ k * hermiteFun1 k x