← Mathematical handbook

theorem Verification.gaussianScaleMixtureLaw_comparison (r : ℝ) (μ : MeasureTheory.ProbabilityMeasure ℝ) (s : ℝ → ℝ) (hs : Measurable s) (hp : ∀ᵐ (t : ℝ) ∂↑μ, 0 < s t) : have L := ↑(ProbabilityTheory.Copula.gaussianScaleMixtureLaw (bivariateCorrelation r) μ s); (L.prod L).real {p : (Fin 2 → ℝ) × (Fin 2 → ℝ) | p.1 ≤ p.2} = (ProbabilityTheory.multivariateGaussian 0 (bivariateCorrelation r)).real {x : EuclideanSpace ℝ (Fin 2) | x.ofLp 0 ≤ 0 ∧ x.ofLp 1 ≤ 0}