← Copula mathematical handbook

Invariance of the copula under monotone transformations

Nelsen, An Introduction to Copulas, second edition, Theorems 2.4.3 and 2.4.4.

Let μ be a law on Fin d → ℝ with continuous marginal CDFs and let each coordinate be transformed by a strictly monotone function f i. If s is the set of coordinates with strictly decreasing f i, then the transformed law again has continuous marginal CDFs and its copula is the copula of μ reflected in the coordinates of s (ofContinuousMarginals_map_coordMap).

For d = 2 this gives the classical statements: two increasing transformations leave the copula unchanged, one decreasing transformation reflects the corresponding coordinate, and two decreasing transformations produce the survival copula.

def ProbabilityTheory.Copula.coordMap {d : ℕ} (f : Fin d → ℝ → ℝ) (x : Fin d → ℝ) : Fin d → ℝ

Apply the function f i to the i-th coordinate of a real vector.

Equations

• ProbabilityTheory.Copula.coordMap f x i = f i (x i)

@[simp]

theorem ProbabilityTheory.Copula.coordMap_apply {d : ℕ} (f : Fin d → ℝ → ℝ) (x : Fin d → ℝ) (i : Fin d) : coordMap f x i = f i (x i)

theorem ProbabilityTheory.Copula.measurable_coordMap {d : ℕ} {f : Fin d → ℝ → ℝ} (hf : ∀ (i : Fin d), Measurable (f i)) : Measurable (coordMap f)

Coordinatewise application of measurable maps is measurable.

theorem ProbabilityTheory.Copula.measurable_fn_of_strict {d : ℕ} {s : Finset (Fin d)} {f : Fin d → ℝ → ℝ} (hinc : ∀ i ∉ s, StrictMono (f i)) (hdec : ∀ i ∈ s, StrictAnti (f i)) (i : Fin d) : Measurable (f i)

Strictly monotone functions, of either direction, are measurable.

theorem ProbabilityTheory.Copula.measure_singleton_eq_zero_of_continuous_cdf (m : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure m] (hc : Continuous ↑(ProbabilityTheory.cdf m)) (x : ℝ) : m {x} = 0

A real probability measure with continuous CDF has no atoms.

theorem ProbabilityTheory.Copula.real_Ici_eq_one_sub (m : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure m] {x : ℝ} (h : m {x} = 0) : m.real (Set.Ici x) = 1 - m.real (Set.Iic x)

For an atomless probability measure, m [x, ∞) = 1 - m (-∞, x].

theorem ProbabilityTheory.Copula.marginal_map_coordMap {d : ℕ} (μ : MeasureTheory.ProbabilityMeasure (Fin d → ℝ)) {f : Fin d → ℝ → ℝ} (hf : ∀ (i : Fin d), Measurable (f i)) (i : Fin d) : marginal (μ.map (coordMap f)) i = MeasureTheory.Measure.map (f i) (marginal μ i)

The marginals of a coordinatewise transformed law are the transformed marginals.

theorem ProbabilityTheory.Copula.cdf_marginal_map_coordMap_of_strictMono {d : ℕ} (μ : MeasureTheory.ProbabilityMeasure (Fin d → ℝ)) {f : Fin d → ℝ → ℝ} (hf : ∀ (i : Fin d), Measurable (f i)) {i : Fin d} (hi : StrictMono (f i)) (x : ℝ) : ↑(ProbabilityTheory.cdf (marginal (μ.map (coordMap f)) i)) (f i x) = ↑(ProbabilityTheory.cdf (marginal μ i)) x

theorem ProbabilityTheory.Copula.cdf_marginal_map_coordMap_of_strictAnti {d : ℕ} (μ : MeasureTheory.ProbabilityMeasure (Fin d → ℝ)) {f : Fin d → ℝ → ℝ} (hf : ∀ (i : Fin d), Measurable (f i)) {i : Fin d} (hi : StrictAnti (f i)) (hc : Continuous ↑(ProbabilityTheory.cdf (marginal μ i))) (x : ℝ) : ↑(ProbabilityTheory.cdf (marginal (μ.map (coordMap f)) i)) (f i x) = 1 - ↑(ProbabilityTheory.cdf (marginal μ i)) x

theorem ProbabilityTheory.Copula.continuous_cdf_marginal_map_coordMap {d : ℕ} (μ : MeasureTheory.ProbabilityMeasure (Fin d → ℝ)) (hc : ∀ (i : Fin d), Continuous ↑(ProbabilityTheory.cdf (marginal μ i))) {f : Fin d → ℝ → ℝ} {s : Finset (Fin d)} (hinc : ∀ i ∉ s, StrictMono (f i)) (hdec : ∀ i ∈ s, StrictAnti (f i)) (i : Fin d) : Continuous ↑(ProbabilityTheory.cdf (marginal (μ.map (coordMap f)) i))

Transforming every coordinate by a strictly monotone function keeps the marginal CDFs continuous, because an injective map sends an atomless law to an atomless law.

theorem ProbabilityTheory.Copula.marginalTransform_coordMap {d : ℕ} (μ : MeasureTheory.ProbabilityMeasure (Fin d → ℝ)) (hc : ∀ (i : Fin d), Continuous ↑(ProbabilityTheory.cdf (marginal μ i))) {f : Fin d → ℝ → ℝ} {s : Finset (Fin d)} (hinc : ∀ i ∉ s, StrictMono (f i)) (hdec : ∀ i ∈ s, StrictAnti (f i)) (x : Fin d → ℝ) : marginalTransform (μ.map (coordMap f)) (coordMap f x) = reflectPoint s (marginalTransform μ x)

The coordinatewise transform of the marginal CDFs of the image law is the reflection of the transform of the original law.

theorem ProbabilityTheory.Copula.ofContinuousMarginals_map_coordMap {d : ℕ} (μ : MeasureTheory.ProbabilityMeasure (Fin d → ℝ)) (hc : ∀ (i : Fin d), Continuous ↑(ProbabilityTheory.cdf (marginal μ i))) {f : Fin d → ℝ → ℝ} {s : Finset (Fin d)} (hinc : ∀ i ∉ s, StrictMono (f i)) (hdec : ∀ i ∈ s, StrictAnti (f i)) : ofContinuousMarginals (μ.map (coordMap f)) ⋯ = (ofContinuousMarginals μ hc).reflect s

Nelsen, Theorems 2.4.3 and 2.4.4 (any dimension). Applying strictly increasing maps to the coordinates outside s and strictly decreasing maps to the coordinates in s replaces the copula by its reflection in the coordinates of s.

theorem ProbabilityTheory.Copula.isSklarCopula_map_coordMap {d : ℕ} {μ : MeasureTheory.ProbabilityMeasure (Fin d → ℝ)} (hc : ∀ (i : Fin d), Continuous ↑(ProbabilityTheory.cdf (marginal μ i))) {f : Fin d → ℝ → ℝ} {s : Finset (Fin d)} (hinc : ∀ i ∉ s, StrictMono (f i)) (hdec : ∀ i ∈ s, StrictAnti (f i)) {C : Copula d} (hC : IsSklarCopula μ C) : IsSklarCopula (μ.map (coordMap f)) (C.reflect s)

Any Sklar copula of μ reflected in s is a Sklar copula of the transformed law.

theorem ProbabilityTheory.Copula.eq_reflect_of_isSklarCopula_map_coordMap {d : ℕ} {μ : MeasureTheory.ProbabilityMeasure (Fin d → ℝ)} (hc : ∀ (i : Fin d), Continuous ↑(ProbabilityTheory.cdf (marginal μ i))) {f : Fin d → ℝ → ℝ} {s : Finset (Fin d)} (hinc : ∀ i ∉ s, StrictMono (f i)) (hdec : ∀ i ∈ s, StrictAnti (f i)) {C D : Copula d} (hC : IsSklarCopula μ C) (hD : IsSklarCopula (μ.map (coordMap f)) D) : D = C.reflect s

The Sklar copula of the transformed law is the reflected copula of the original law.

The bivariate statements

theorem ProbabilityTheory.Copula.isSklarCopula_map_strictMono_two {μ : MeasureTheory.ProbabilityMeasure (Fin 2 → ℝ)} (hc : ∀ (i : Fin 2), Continuous ↑(ProbabilityTheory.cdf (marginal μ i))) {C : Copula 2} (hC : IsSklarCopula μ C) {α β : ℝ → ℝ} (hα : StrictMono α) (hβ : StrictMono β) : IsSklarCopula (μ.map (coordMap ![α, β])) C

Nelsen, Theorem 2.4.3. Strictly increasing transformations of both coordinates leave the Sklar copula unchanged.

theorem ProbabilityTheory.Copula.isSklarCopula_map_strictMono_strictAnti {μ : MeasureTheory.ProbabilityMeasure (Fin 2 → ℝ)} (hc : ∀ (i : Fin 2), Continuous ↑(ProbabilityTheory.cdf (marginal μ i))) {C : Copula 2} (hC : IsSklarCopula μ C) {α β : ℝ → ℝ} (hα : StrictMono α) (hβ : StrictAnti β) : IsSklarCopula (μ.map (coordMap ![α, β])) (C.reflect {1})

Nelsen, Theorem 2.4.4 (first case). A strictly increasing map of the first coordinate and a strictly decreasing map of the second coordinate reflect the second copula coordinate.

theorem ProbabilityTheory.Copula.isSklarCopula_map_strictAnti_strictMono {μ : MeasureTheory.ProbabilityMeasure (Fin 2 → ℝ)} (hc : ∀ (i : Fin 2), Continuous ↑(ProbabilityTheory.cdf (marginal μ i))) {C : Copula 2} (hC : IsSklarCopula μ C) {α β : ℝ → ℝ} (hα : StrictAnti α) (hβ : StrictMono β) : IsSklarCopula (μ.map (coordMap ![α, β])) (C.reflect {0})

Nelsen, Theorem 2.4.4 (second case). A strictly decreasing map of the first coordinate and a strictly increasing map of the second coordinate reflect the first copula coordinate.

theorem ProbabilityTheory.Copula.isSklarCopula_map_strictAnti_two {μ : MeasureTheory.ProbabilityMeasure (Fin 2 → ℝ)} (hc : ∀ (i : Fin 2), Continuous ↑(ProbabilityTheory.cdf (marginal μ i))) {C : Copula 2} (hC : IsSklarCopula μ C) {α β : ℝ → ℝ} (hα : StrictAnti α) (hβ : StrictAnti β) : IsSklarCopula (μ.map (coordMap ![α, β])) C.survivalCopula

Nelsen, Theorem 2.4.4 (survival case). Strictly decreasing transformations of both coordinates turn the Sklar copula into the survival copula.