← Mathematical handbook

theorem Verification.gaussian_normalCDF_product_integral {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) (a b c : ℝ) (hb : 0 < b) (hc : 0 < c) : ∫ (p : ℝ × ℝ), ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1)) (a * p.1 / b) * ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1)) (a * (r * p.1 + √(1 - r ^ 2) * p.2) / c) ∂(ProbabilityTheory.gaussianReal 0 1).prod (ProbabilityTheory.gaussianReal 0 1) = 1 / 4 + Real.arcsin (r * a ^ 2 / (√(a ^ 2 + b ^ 2) * √(a ^ 2 + c ^ 2))) / (2 * Real.pi)

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

Equations

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

theorem Verification.map_gaussianRealPair {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) : MeasureTheory.Measure.map (⇑(gaussianRealPair r)) ((ProbabilityTheory.gaussianReal 0 1).prod (ProbabilityTheory.gaussianReal 0 1)) = ProbabilityTheory.multivariateGaussian 0 (bivariateCorrelation r)

theorem Verification.gaussian_cdf_product_integral {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) (a b c : ℝ) (hb : 0 < b) (hc : 0 < c) : ∫ (x : EuclideanSpace ℝ (Fin 2)), ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1)) (a * x.ofLp 0 / b) * ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1)) (a * x.ofLp 1 / c) ∂ProbabilityTheory.multivariateGaussian 0 (bivariateCorrelation r) = 1 / 4 + Real.arcsin (r * a ^ 2 / (√(a ^ 2 + b ^ 2) * √(a ^ 2 + c ^ 2))) / (2 * Real.pi)