← Mathematical handbook

theorem Verification.standardGaussian_lower_triangle {r : ℝ} (hr : r ∈ Set.Ioo (-1) 1) (a : ℝ) : ((ProbabilityTheory.gaussianReal 0 1).prod (ProbabilityTheory.gaussianReal 0 1)).real {p : ℝ × ℝ | p.1 ≤ a ∧ r * p.1 + √(1 - r ^ 2) * p.2 ≤ p.1} = ∫ (x : ℝ) in Set.Iic a, ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1)) ((x - r * x) / √(1 - r ^ 2)) ∂ProbabilityTheory.gaussianReal 0 1

theorem Verification.gaussianBivariate_triangle_normal {r : ℝ} (hr : r ∈ Set.Ioo (-1) 1) (a : ℝ) : (gaussianBivariate r ⋯).toMeasure.real {u : Fin 2 → ↑unitInterval | u 0 ≤ ProbabilityTheory.cdfUnit (ProbabilityTheory.gaussianReal 0 1) a ∧ u 1 ≤ u 0} = ∫ (x : ℝ) in Set.Iic a, ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1)) ((x - r * x) / √(1 - r ^ 2)) ∂ProbabilityTheory.gaussianReal 0 1

theorem Verification.symmetricCopula_diagonal_le_triangle (C : ProbabilityTheory.Copula 2) (hC : C.transpose = C) (t : ↑unitInterval) : C.diagonal t ≤ 2 * C.toMeasure.real {u : Fin 2 → ↑unitInterval | u 0 ≤ t ∧ u 1 ≤ u 0}

theorem Verification.normalQuantile_tendsto_zero : Filter.Tendsto normalQuantile (nhdsWithin 0 (Set.Ioi 0)) Filter.atBot

theorem Verification.gaussianBivariate_diagonal_normal_bound {r : ℝ} (hr : r ∈ Set.Ioo (-1) 1) (a : ℝ) : (gaussianBivariate r ⋯).diagonal (ProbabilityTheory.cdfUnit (ProbabilityTheory.gaussianReal 0 1) a) ≤ 2 * ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1)) a * ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1)) ((1 - r) / √(1 - r ^ 2) * a)

theorem Verification.gaussianBivariate_radiallySymmetric {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) : (gaussianBivariate r hr).IsRadiallySymmetric

theorem Verification.gaussianBivariate_lowerTail_zero {r : ℝ} (hr : r ∈ Set.Ioo (-1) 1) : (gaussianBivariate r ⋯).HasLowerTailDependence 0

theorem Verification.gaussianBivariate_lowerTail {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) : (gaussianBivariate r hr).HasLowerTailDependence (if r = 1 then 1 else 0)

theorem Verification.gaussianBivariate_upperTail {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) : (gaussianBivariate r hr).HasUpperTailDependence (if r = 1 then 1 else 0)