theorem
Verification.gaussianScaleMixture_cdf_marginal
{r : ℝ}
(hr : r ∈ Set.Icc (-1) 1)
(μ : MeasureTheory.ProbabilityMeasure ℝ)
(s : ℝ → ℝ)
(hs : Measurable s)
(hp : ∀ᵐ (t : ℝ) ∂↑μ, 0 < s t)
(a b : ℝ)
:
(ProbabilityTheory.Copula.gaussianScaleMixture (bivariateCorrelation r) ⋯ ⋯ μ s hs hp).cdf
![ProbabilityTheory.cdfUnit (normalScaleMixtureMarginal μ s) a, ProbabilityTheory.cdfUnit (normalScaleMixtureMarginal μ s) b] = ∫ (t : ℝ), (gaussianBivariate r hr).cdf
![ProbabilityTheory.cdfUnit (ProbabilityTheory.gaussianReal 0 1) (a / s t), ProbabilityTheory.cdfUnit (ProbabilityTheory.gaussianReal 0 1) (b / s t)] ∂↑μ
theorem
Verification.gaussianScaleMixture_cdf_continuous
(μ : MeasureTheory.ProbabilityMeasure ℝ)
(s : ℝ → ℝ)
(hs : Measurable s)
(hp : ∀ᵐ (t : ℝ) ∂↑μ, 0 < s t)
(u : Fin 2 → ↑unitInterval)
:
Continuous fun (r : ↑(Set.Icc (-1) 1)) =>
(ProbabilityTheory.Copula.gaussianScaleMixture (bivariateCorrelation ↑r) ⋯ ⋯ μ s hs hp).cdf u