← Copula mathematical handbook

Symmetry of random vectors and of their copulas

Nelsen, An Introduction to Copulas, second edition, §2.7 (Theorems 2.7.1 and 2.7.2 in the formulation for laws on Fin 2 → ℝ).

• A law μ is exchangeable if it is invariant under swapCoord. Then its coordinate laws agree and every Sklar copula of μ is exchangeable. Conversely, an exchangeable Sklar copula together with equal coordinate laws gives an exchangeable law.
• A law is radially symmetric about (a, b) if it is invariant under reflectAbout a b. With continuous marginals, every Sklar copula is then radially symmetric. Conversely, a radially symmetric Sklar copula together with marginals symmetric about a and b gives a radially symmetric law.

Laws are compared through their underlying measures in the converse directions.

def ProbabilityTheory.Copula.swapCoord (x : Fin 2 → ℝ) : Fin 2 → ℝ

Exchange the two coordinates of a real vector.

Equations

• ProbabilityTheory.Copula.swapCoord x i = x (![1, 0] i)

theorem ProbabilityTheory.Copula.measurable_swapCoord : Measurable swapCoord

@[reducible, inline]

abbrev ProbabilityTheory.Copula.reflectAbout (a b : ℝ) : (Fin 2 → ℝ) → Fin 2 → ℝ

Reflection of a plane vector through the point (a, b).

Equations

• ProbabilityTheory.Copula.reflectAbout a b = ProbabilityTheory.Copula.coordMap ![fun (x : ℝ) => 2 * a - x, fun (x : ℝ) => 2 * b - x]

theorem ProbabilityTheory.Copula.strictAnti_two_mul_sub (a : ℝ) : StrictAnti fun (x : ℝ) => 2 * a - x

theorem ProbabilityTheory.Copula.marginal_map_swapCoord (μ : MeasureTheory.ProbabilityMeasure (Fin 2 → ℝ)) (i : Fin 2) : marginal (μ.map swapCoord) i = marginal μ (![1, 0] i)

The coordinate laws of the swapped law are the swapped coordinate laws.

theorem ProbabilityTheory.Copula.isSklarCopula_map_swapCoord {μ : MeasureTheory.ProbabilityMeasure (Fin 2 → ℝ)} {C : Copula 2} (hC : IsSklarCopula μ C) : IsSklarCopula (μ.map swapCoord) C.transpose

Swapping the coordinates of a law transposes each of its Sklar copulas.

theorem ProbabilityTheory.Copula.marginal_zero_eq_one_of_map_swapCoord_eq {μ : MeasureTheory.ProbabilityMeasure (Fin 2 → ℝ)} (h : μ.map swapCoord = μ) : marginal μ 0 = marginal μ 1

An exchangeable random vector has identical coordinate laws.

theorem ProbabilityTheory.Copula.isExchangeable_of_map_swapCoord_eq {μ : MeasureTheory.ProbabilityMeasure (Fin 2 → ℝ)} (hc : ∀ (i : Fin 2), Continuous ↑(ProbabilityTheory.cdf (marginal μ i))) {C : Copula 2} (hC : IsSklarCopula μ C) (h : μ.map swapCoord = μ) : C.IsExchangeable

Nelsen, §2.7 (exchangeable random vectors). Every Sklar copula of an exchangeable law with continuous marginals is exchangeable.

theorem ProbabilityTheory.Copula.map_swapCoord_eq_of_isExchangeable {μ : MeasureTheory.ProbabilityMeasure (Fin 2 → ℝ)} {C : Copula 2} (hC : IsSklarCopula μ C) (hCs : C.IsExchangeable) (hm : marginal μ 0 = marginal μ 1) : MeasureTheory.Measure.map swapCoord ↑μ = ↑μ

An exchangeable Sklar copula and equal coordinate laws give an exchangeable law.

theorem ProbabilityTheory.Copula.isRadiallySymmetric_of_map_reflectAbout_eq {μ : MeasureTheory.ProbabilityMeasure (Fin 2 → ℝ)} (hc : ∀ (i : Fin 2), Continuous ↑(ProbabilityTheory.cdf (marginal μ i))) {C : Copula 2} (hC : IsSklarCopula μ C) {a b : ℝ} (h : μ.map (reflectAbout a b) = μ) : C.IsRadiallySymmetric

Nelsen, §2.7 (radially symmetric random vectors). Every Sklar copula of a law with continuous marginals that is radially symmetric about (a, b) is radially symmetric.

theorem ProbabilityTheory.Copula.map_reflectAbout_eq_of_isRadiallySymmetric {μ : MeasureTheory.ProbabilityMeasure (Fin 2 → ℝ)} (hc : ∀ (i : Fin 2), Continuous ↑(ProbabilityTheory.cdf (marginal μ i))) {C : Copula 2} (hC : IsSklarCopula μ C) (hCs : C.IsRadiallySymmetric) {a b : ℝ} (hm0 : MeasureTheory.Measure.map (fun (x : ℝ) => 2 * a - x) (marginal μ 0) = marginal μ 0) (hm1 : MeasureTheory.Measure.map (fun (x : ℝ) => 2 * b - x) (marginal μ 1) = marginal μ 1) : MeasureTheory.Measure.map (reflectAbout a b) ↑μ = ↑μ

A radially symmetric Sklar copula and coordinate laws symmetric about a and b give a law that is radially symmetric about (a, b).