← Mathematical handbook

Differences of centered Gaussian pairs with different correlations

theorem Verification.charFun_bivariateGaussian {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) (t : EuclideanSpace ℝ (Fin 2)) : MeasureTheory.charFun (ProbabilityTheory.multivariateGaussian 0 (bivariateCorrelation r)) t = Complex.exp (-↑(t.ofLp 0 ^ 2 + 2 * r * t.ofLp 0 * t.ofLp 1 + t.ofLp 1 ^ 2) / 2)

theorem Verification.map_gaussianDifference_mixed {r s : ℝ} (hr : r ∈ Set.Icc (-1) 1) (hs : s ∈ Set.Icc (-1) 1) : MeasureTheory.Measure.map (⇑gaussianDifference) ((ProbabilityTheory.multivariateGaussian 0 (bivariateCorrelation r)).prod (ProbabilityTheory.multivariateGaussian 0 (bivariateCorrelation s))) = ProbabilityTheory.multivariateGaussian 0 (bivariateCorrelation ((r + s) / 2))