← Mathematical handbook

theorem Verification.gaussian_mixtureCDF_product_integral {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) (μ : MeasureTheory.ProbabilityMeasure ℝ) (s : ℝ → ℝ) (hs : Measurable s) (hp : ∀ᵐ (t : ℝ) ∂↑μ, 0 < s t) (a : ℝ) : ∫ (x : EuclideanSpace ℝ (Fin 2)), ↑(ProbabilityTheory.cdf (normalScaleMixtureMarginal μ s)) (a * x.ofLp 0) * ↑(ProbabilityTheory.cdf (normalScaleMixtureMarginal μ s)) (a * x.ofLp 1) ∂ProbabilityTheory.multivariateGaussian 0 (bivariateCorrelation r) = ∫ (t : ℝ × ℝ), 1 / 4 + Real.arcsin (r * a ^ 2 / (√(a ^ 2 + s t.1 ^ 2) * √(a ^ 2 + s t.2 ^ 2))) / (2 * Real.pi) ∂(↑μ).prod ↑μ

theorem Verification.gaussianScaleMixture_spearmanRho_integral {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) (μ : MeasureTheory.ProbabilityMeasure ℝ) (s : ℝ → ℝ) (hs : Measurable s) (hp : ∀ᵐ (t : ℝ) ∂↑μ, 0 < s t) : (ProbabilityTheory.Copula.gaussianScaleMixture (bivariateCorrelation r) ⋯ ⋯ μ s hs hp).spearmanRho = 12 * ∫ (a : ℝ), ∫ (t : ℝ × ℝ), 1 / 4 + Real.arcsin (r * s a ^ 2 / (√(s a ^ 2 + s t.1 ^ 2) * √(s a ^ 2 + s t.2 ^ 2))) / (2 * Real.pi) ∂(↑μ).prod ↑μ ∂↑μ - 3

theorem Verification.integrable_arcsin_comp {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] (f : α → ℝ) (hf : Measurable f) : MeasureTheory.Integrable (fun (x : α) => Real.arcsin (f x)) μ

theorem Verification.gaussianScaleMixture_spearmanRho {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) (μ : MeasureTheory.ProbabilityMeasure ℝ) (s : ℝ → ℝ) (hs : Measurable s) (hp : ∀ᵐ (t : ℝ) ∂↑μ, 0 < s t) : (ProbabilityTheory.Copula.gaussianScaleMixture (bivariateCorrelation r) ⋯ ⋯ μ s hs hp).spearmanRho = 6 / Real.pi * ∫ (a : ℝ), ∫ (t : ℝ × ℝ), Real.arcsin (r * s a ^ 2 / (√(s a ^ 2 + s t.1 ^ 2) * √(s a ^ 2 + s t.2 ^ 2))) ∂(↑μ).prod ↑μ ∂↑μ