noncomputable def GaussianSpace.addSmulCLM {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (a b : ℝ) : E × E →L[ℝ] E

theorem GaussianSpace.gaussian_sum_pushforward {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (a b c : ℝ) (habc : a ^ 2 + b ^ 2 = c ^ 2) : MeasureTheory.Measure.map (⇑(addSmulCLM a b)) ((ProbabilityTheory.stdGaussian E).prod (ProbabilityTheory.stdGaussian E)) = MeasureTheory.Measure.map (⇑(c • ContinuousLinearMap.id ℝ E)) (ProbabilityTheory.stdGaussian E)

theorem GaussianSpace.integral_gaussian_sum {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (a b c : ℝ) (habc : a ^ 2 + b ^ 2 = c ^ 2) (g : E → ℝ) (hg_meas : Measurable g) (hg_int : MeasureTheory.Integrable (g ∘ ⇑(addSmulCLM a b)) ((ProbabilityTheory.stdGaussian E).prod (ProbabilityTheory.stdGaussian E))) : ∫ (w : E), ∫ (v : E), g (a • w + b • v) ∂ProbabilityTheory.stdGaussian E ∂ProbabilityTheory.stdGaussian E = ∫ (u : E), g (c • u) ∂ProbabilityTheory.stdGaussian E

theorem GaussianSpace.ornsteinUhlenbeckOp_comp {n : ℕ} (ρ σ : ℝ) (hρ : ρ ∈ Set.Icc (-1) 1) (hσ : σ ∈ Set.Icc (-1) 1) (f : EuclideanSpace ℝ (Fin n) → ℝ) (hf : Measurable f) (hf_int : ∀ (v : EuclideanSpace ℝ (Fin n)), MeasureTheory.Integrable (fun (u : EuclideanSpace ℝ (Fin n)) => f (v + √(1 - (ρ * σ) ^ 2) • u)) (ProbabilityTheory.stdGaussian (EuclideanSpace ℝ (Fin n)))) : (ornsteinUhlenbeckOp ρ fun (x : EuclideanSpace ℝ (Fin n)) => ornsteinUhlenbeckOp σ f x) = ornsteinUhlenbeckOp (ρ * σ) f