← Mathematical handbook

theorem Verification.gaussianScaleMixture_absolutelyContinuous {r : ℝ} (hr : r ∈ Set.Ioo (-1) 1) (μ : MeasureTheory.ProbabilityMeasure ℝ) (s : ℝ → ℝ) (hs : Measurable s) (hp : ∀ᵐ (t : ℝ) ∂↑μ, 0 < s t) : (ProbabilityTheory.Copula.gaussianScaleMixture (bivariateCorrelation r) ⋯ ⋯ μ s hs hp).toMeasure.AbsolutelyContinuous MeasureTheory.volume

theorem Verification.gaussianScaleMixture_absolutelyContinuous_iff {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).toMeasure.AbsolutelyContinuous MeasureTheory.volume ↔ r ∈ Set.Ioo (-1) 1