← Mathematical handbook

A Gaussian representation for the squared conditional-CDF integral

theorem Verification.charFunDual_standardNormal (L : StrongDual ℝ ℝ) : MeasureTheory.charFunDual (ProbabilityTheory.gaussianReal 0 1) L = Complex.exp (-↑(L 1 ^ 2) / 2)

noncomputable def Verification.gaussianXiMap (r : ℝ) : (ℝ × ℝ) × ℝ × ℝ →L[ℝ] EuclideanSpace ℝ (Fin 2)

Equations

• One or more equations did not get rendered due to their size.

theorem Verification.map_gaussianXiMap {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) : MeasureTheory.Measure.map (⇑(gaussianXiMap r)) (((ProbabilityTheory.gaussianReal 0 1).prod (ProbabilityTheory.gaussianReal 0 1)).prod ((ProbabilityTheory.gaussianReal 0 1).prod (ProbabilityTheory.gaussianReal 0 1))) = ProbabilityTheory.multivariateGaussian 0 (bivariateCorrelation ((1 + r ^ 2) / 2))