theorem
Verification.gaussianScaleMixture_transpose
{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).transpose = ProbabilityTheory.Copula.gaussianScaleMixture (bivariateCorrelation r) ⋯ ⋯ μ s hs hp
theorem
Verification.gaussianScaleMixture_radiallySymmetric
{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).IsRadiallySymmetric