← Mathematical handbook

theorem Verification.gaussianScaleMixture_toMeasure {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 = MeasureTheory.Measure.map (fun (p : EuclideanSpace ℝ (Fin 2) × ℝ) (i : Fin 2) => ProbabilityTheory.cdfUnit (normalScaleMixtureMarginal μ s) (s p.2 * p.1.ofLp i)) ((ProbabilityTheory.multivariateGaussian 0 (bivariateCorrelation r)).prod ↑μ)

theorem Verification.normalScaleMixtureMarginal_cdfUnit_neg (μ : MeasureTheory.ProbabilityMeasure ℝ) (s : ℝ → ℝ) (hs : Measurable s) (hp : ∀ᵐ (t : ℝ) ∂↑μ, 0 < s t) (x : ℝ) : ProbabilityTheory.cdfUnit (normalScaleMixtureMarginal μ s) (-x) = unitInterval.symm (ProbabilityTheory.cdfUnit (normalScaleMixtureMarginal μ s) x)

theorem Verification.gaussianScaleMixture_neg {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 = (ProbabilityTheory.Copula.gaussianScaleMixture (bivariateCorrelation r) ⋯ ⋯ μ s hs hp).reflect {1}

theorem Verification.studentBivariate_neg {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) (ν : ℝ) (hν : 0 < ν) : studentBivariate (-r) ⋯ ν hν = (studentBivariate r hr ν hν).reflect {1}