← Mathematical handbook

Centered bivariate Gaussian quadrant probabilities

The checked half-line normal-CDF integral evaluates the mixed-sign quadrant. The standard normal marginal then gives the lower quadrant. We also establish strict CDF monotonicity to transfer comparisons through the copula transform.

theorem Verification.standardNormalCDF_strictMono : StrictMono ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1))

theorem Verification.standardGaussian_linear_halfline {s : ℝ} (hs : 0 < s) (b : ℝ) : ∫ (y : ℝ), if s * y ≤ b then 1 else 0 ∂ProbabilityTheory.gaussianReal 0 1 = ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1)) (b / s)

theorem Verification.standardGaussian_discordant_quadrant {r : ℝ} (hr : r ∈ Set.Ioo (-1) 1) : ((ProbabilityTheory.gaussianReal 0 1).prod (ProbabilityTheory.gaussianReal 0 1)).real {p : ℝ × ℝ | 0 < p.1 ∧ r * p.1 + √(1 - r ^ 2) * p.2 ≤ 0} = 1 / 4 - Real.arcsin r / (2 * Real.pi)

theorem Verification.multivariateGaussian_discordant_quadrant {r : ℝ} (hr : r ∈ Set.Ioo (-1) 1) : (ProbabilityTheory.multivariateGaussian 0 (bivariateCorrelation r)).real {x : EuclideanSpace ℝ (Fin 2) | 0 < x.ofLp 0 ∧ x.ofLp 1 ≤ 0} = 1 / 4 - Real.arcsin r / (2 * Real.pi)

theorem Verification.multivariateGaussian_lower_quadrant {r : ℝ} (hr : r ∈ Set.Ioo (-1) 1) : (ProbabilityTheory.multivariateGaussian 0 (bivariateCorrelation r)).real {x : EuclideanSpace ℝ (Fin 2) | x.ofLp 0 ≤ 0 ∧ x.ofLp 1 ≤ 0} = 1 / 4 + Real.arcsin r / (2 * Real.pi)