← Mathematical handbook

The conditional CDF of a Gaussian copula in normal coordinates

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

theorem Verification.gaussianBivariate_cdf_normal {r : ℝ} (hr : r ∈ Set.Ioo (-1) 1) (a b : ℝ) : (gaussianBivariate r ⋯).cdf ![ProbabilityTheory.cdfUnit (ProbabilityTheory.gaussianReal 0 1) a, ProbabilityTheory.cdfUnit (ProbabilityTheory.gaussianReal 0 1) b] = ∫ (x : ℝ) in Set.Iic a, ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1)) ((b - r * x) / √(1 - r ^ 2)) ∂ProbabilityTheory.gaussianReal 0 1

theorem Verification.ae_eq_of_nonneg_Iic_integrals {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsFiniteMeasure μ] {f g : ℝ → ℝ} (hf : MeasureTheory.Integrable f μ) (hg : MeasureTheory.Integrable g μ) (hnf : ∀ (x : ℝ), 0 ≤ f x) (hng : ∀ (x : ℝ), 0 ≤ g x) (he : ∀ (a : ℝ), ∫ (x : ℝ) in Set.Iic a, f x ∂μ = ∫ (x : ℝ) in Set.Iic a, g x ∂μ) : f =ᵐ[μ] g

theorem Verification.gaussianBivariate_conditionalCDF_normal {r : ℝ} (hr : r ∈ Set.Ioo (-1) 1) (b : ℝ) : (fun (x : ℝ) => (gaussianBivariate r ⋯).conditionalCDF (ProbabilityTheory.cdfUnit (ProbabilityTheory.gaussianReal 0 1) x) (ProbabilityTheory.cdfUnit (ProbabilityTheory.gaussianReal 0 1) b)) =ᵐ[ProbabilityTheory.gaussianReal 0 1] fun (x : ℝ) => ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1)) ((b - r * x) / √(1 - r ^ 2))

theorem Verification.integral_standardNormal_transform {f : ↑unitInterval → ℝ} (hf : MeasureTheory.AEStronglyMeasurable f MeasureTheory.volume) : ∫ (u : ↑unitInterval), f u = ∫ (x : ℝ), f (ProbabilityTheory.cdfUnit (ProbabilityTheory.gaussianReal 0 1) x) ∂ProbabilityTheory.gaussianReal 0 1

theorem Verification.gaussianBivariate_xi_normal_integral {r : ℝ} (hr : r ∈ Set.Ioo (-1) 1) : (gaussianBivariate r ⋯).chatterjeeXi = 6 * ∫ (b : ℝ), ∫ (x : ℝ), ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1)) ((b - r * x) / √(1 - r ^ 2)) ^ 2 ∂ProbabilityTheory.gaussianReal 0 1 ∂ProbabilityTheory.gaussianReal 0 1 - 2