Documentation

Copula.Symmetry

← Copula mathematical handbook

Exchangeability, radial symmetry and symmetrization #

Copula-level symmetries as in Nelsen, second edition, §2.7.

def ProbabilityTheory.Copula.IsExchangeable (C : Copula 2) :

Exchangeability of the two uniform coordinates.

Equations

C.IsExchangeable = (C.transpose = C)

Instances For

def ProbabilityTheory.Copula.IsRadiallySymmetric (C : Copula 2) :

Invariance under simultaneous reflection of both coordinates.

Equations

C.IsRadiallySymmetric = (C.survivalCopula = C)

Instances For

theorem ProbabilityTheory.Copula.isExchangeable_iff (C : Copula 2) :

C.IsExchangeable ↔ ∀ (u v : ↑unitInterval), C.cdf ![u, v] = C.cdf ![v, u]

theorem ProbabilityTheory.Copula.isRadiallySymmetric_iff (C : Copula 2) :

C.IsRadiallySymmetric ↔ ∀ (u v : ↑unitInterval), C.cdf ![u, v] = ↑u + ↑v - 1 + C.cdf ![unitInterval.symm u, unitInterval.symm v]

theorem ProbabilityTheory.Copula.transpose_survivalCopula (C : Copula 2) :

C.survivalCopula.transpose = C.transpose.survivalCopula

theorem ProbabilityTheory.Copula.transpose_mix (C D : Copula 2) (a : ↑unitInterval) :

(C.mix D a).transpose = C.transpose.mix D.transpose a

theorem ProbabilityTheory.Copula.survivalCopula_mix (C D : Copula 2) (a : ↑unitInterval) :

(C.mix D a).survivalCopula = C.survivalCopula.mix D.survivalCopula a

theorem ProbabilityTheory.Copula.IsExchangeable.mix {C D : Copula 2} (hC : C.IsExchangeable) (hD : D.IsExchangeable) (a : ↑unitInterval) :

(C.mix D a).IsExchangeable

theorem ProbabilityTheory.Copula.IsRadiallySymmetric.mix {C D : Copula 2} (hC : C.IsRadiallySymmetric) (hD : D.IsRadiallySymmetric) (a : ↑unitInterval) :

(C.mix D a).IsRadiallySymmetric

theorem ProbabilityTheory.Copula.isExchangeable_symmetrize (C : Copula 2) :

(C.mix C.transpose unitHalf).IsExchangeable

Averaging a copula with its transpose produces an exchangeable copula.

theorem ProbabilityTheory.Copula.isRadiallySymmetric_symmetrize (C : Copula 2) :

(C.mix C.survivalCopula unitHalf).IsRadiallySymmetric

Averaging with the survival copula produces radial symmetry.

theorem ProbabilityTheory.Copula.isExchangeable_fgm (θ : ℝ) (hθ : |θ| ≤ 1) :

(fgm θ hθ).IsExchangeable

theorem ProbabilityTheory.Copula.isRadiallySymmetric_fgm (θ : ℝ) (hθ : |θ| ≤ 1) :

(fgm θ hθ).IsRadiallySymmetric

theorem ProbabilityTheory.Copula.isExchangeable_independence :

(independence 2).IsExchangeable

theorem ProbabilityTheory.Copula.isRadiallySymmetric_independence :

(independence 2).IsRadiallySymmetric

theorem ProbabilityTheory.Copula.isExchangeable_comonotonic :

(comonotonic 2).IsExchangeable

theorem ProbabilityTheory.Copula.isRadiallySymmetric_comonotonic :

(comonotonic 2).IsRadiallySymmetric

theorem ProbabilityTheory.Copula.isExchangeable_countermonotonic :

countermonotonic.IsExchangeable

theorem ProbabilityTheory.Copula.isRadiallySymmetric_countermonotonic :

countermonotonic.IsRadiallySymmetric