← Copula mathematical handbook

Symmetries of bivariate Gaussian scale mixture copulas

A bivariate Gaussian scale mixture S · (G₁, G₂) with G ~ N(0, !![1, r; r, 1]) has a law that is invariant under swapping the coordinates and under x ↦ −x. By the random-vector criteria of Copula.RandomVariable.Symmetry (Nelsen 2006, §2.7), its copula is exchangeable and radially symmetric. This applies to the Student-t, Cauchy, variance-gamma, Laplace, slash and normal–lognormal copulas.

Main results

• gaussianScaleMixtureLaw_corrMatrix_eq: the mixture law is the law of s(T) · (X, Y) with (X, Y) ~ bivariateNormal r independent of T.
• isExchangeable_gaussianScaleMixture, isRadiallySymmetric_gaussianScaleMixture, and the Student-t instances.

theorem ProbabilityTheory.Copula.map_multivariateGaussian_corrMatrix {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) : MeasureTheory.Measure.map (fun (g : EuclideanSpace ℝ (Fin 2)) => (g.ofLp 0, g.ofLp 1)) (multivariateGaussian 0 (corrMatrix r)) = bivariateNormal r

The coordinates of N(0, corrMatrix r) have the law bivariateNormal r.

noncomputable def ProbabilityTheory.Copula.scalePair (s : ℝ → ℝ) (p : (ℝ × ℝ) × ℝ) : Fin 2 → ℝ

The scaling map ((x, y), t) ↦ (s(t) x, s(t) y).

Equations

• ProbabilityTheory.Copula.scalePair s p = ![s p.2 * p.1.1, s p.2 * p.1.2]

theorem ProbabilityTheory.Copula.measurable_scalePair {s : ℝ → ℝ} (hs : Measurable s) : Measurable (scalePair s)

theorem ProbabilityTheory.Copula.gaussianScaleMixtureLaw_corrMatrix_eq {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) (μ : MeasureTheory.ProbabilityMeasure ℝ) {s : ℝ → ℝ} (hs : Measurable s) : ↑(gaussianScaleMixtureLaw (corrMatrix r) μ s) = MeasureTheory.Measure.map (scalePair s) ((bivariateNormal r).prod ↑μ)

The bivariate Gaussian scale mixture law, written with the explicit bivariate normal law.

theorem ProbabilityTheory.Copula.gaussianScaleMixtureLaw_map_swapCoord {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) (μ : MeasureTheory.ProbabilityMeasure ℝ) {s : ℝ → ℝ} (hs : Measurable s) : (gaussianScaleMixtureLaw (corrMatrix r) μ s).map swapCoord = gaussianScaleMixtureLaw (corrMatrix r) μ s

A bivariate Gaussian scale mixture law is exchangeable.

theorem ProbabilityTheory.Copula.gaussianScaleMixtureLaw_map_reflectAbout {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) (μ : MeasureTheory.ProbabilityMeasure ℝ) {s : ℝ → ℝ} (hs : Measurable s) : (gaussianScaleMixtureLaw (corrMatrix r) μ s).map (reflectAbout 0 0) = gaussianScaleMixtureLaw (corrMatrix r) μ s

A bivariate Gaussian scale mixture law is symmetric about the origin.

theorem ProbabilityTheory.Copula.isExchangeable_gaussianScaleMixture {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) (μ : MeasureTheory.ProbabilityMeasure ℝ) (s : ℝ → ℝ) (hs : Measurable s) (hpos : ∀ᵐ (t : ℝ) ∂↑μ, 0 < s t) : (gaussianScaleMixture (corrMatrix r) ⋯ ⋯ μ s hs hpos).IsExchangeable

Bivariate Gaussian scale mixture copulas are exchangeable.

theorem ProbabilityTheory.Copula.isRadiallySymmetric_gaussianScaleMixture {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) (μ : MeasureTheory.ProbabilityMeasure ℝ) (s : ℝ → ℝ) (hs : Measurable s) (hpos : ∀ᵐ (t : ℝ) ∂↑μ, 0 < s t) : (gaussianScaleMixture (corrMatrix r) ⋯ ⋯ μ s hs hpos).IsRadiallySymmetric

Bivariate Gaussian scale mixture copulas are radially symmetric.

theorem ProbabilityTheory.Copula.isExchangeable_studentT {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) (ν : ℝ) (hν : 0 < ν) : (studentT (corrMatrix r) ⋯ ⋯ ν hν).IsExchangeable

The bivariate Student-t copula is exchangeable.

theorem ProbabilityTheory.Copula.isRadiallySymmetric_studentT {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) (ν : ℝ) (hν : 0 < ν) : (studentT (corrMatrix r) ⋯ ⋯ ν hν).IsRadiallySymmetric

The bivariate Student-t copula is radially symmetric.