theorem GaussianStability.gaussianNoiseOperator_eq_ornsteinUhlenbeckOp {n : ℕ} (ρ : ℝ) (f : EuclideanSpace ℝ (Fin n) → ℝ) : gaussianNoiseOperator ρ f = GaussianSpace.ornsteinUhlenbeckOp ρ f