theorem
Verification.gaussianScaleMixtureLaw_marginal
{d : ℕ}
(R : Matrix (Fin d) (Fin d) ℝ)
(hR : R.PosSemidef)
(hd : ∀ (i : Fin d), R i i = 1)
(μ : MeasureTheory.ProbabilityMeasure ℝ)
(s : ℝ → ℝ)
(hs : Measurable s)
(i : Fin d)
:
ProbabilityTheory.Copula.marginal (ProbabilityTheory.Copula.gaussianScaleMixtureLaw R μ s) i = MeasureTheory.Measure.map (fun (p : ℝ × ℝ) => s p.2 * p.1) ((ProbabilityTheory.gaussianReal 0 1).prod ↑μ)