theorem
Verification.gaussianScaleMixture_joint_tp2_density
{r : ℝ}
(hr : r ∈ Set.Ioo (-1) 1)
(μ : MeasureTheory.ProbabilityMeasure ℝ)
(s : ℝ → ℝ)
(hs : Measurable s)
(hp : ∀ᵐ (t : ℝ) ∂↑μ, 0 < s t)
(htp : (ProbabilityTheory.Copula.gaussianScaleMixture (bivariateCorrelation r) ⋯ ⋯ μ s hs hp).HasMTP2Density)
:
∃ (g : ℝ × ℝ → ℝ),
Measurable g ∧ (∀ (p : ℝ × ℝ), 0 ≤ g p) ∧ (∀ (a b c d : ℝ), a ≤ b → c ≤ d → g (a, d) * g (b, c) ≤ g (a, c) * g (b, d)) ∧ MeasureTheory.Measure.map ⇑MeasurableEquiv.finTwoArrow
↑(ProbabilityTheory.Copula.gaussianScaleMixtureLaw (bivariateCorrelation r) μ s) = MeasureTheory.volume.withDensity fun (p : ℝ × ℝ) => ENNReal.ofReal (g p)