← Copula mathematical handbook

Decomposition into general ordinal sums

Nelsen, An Introduction to Copulas, 2nd ed., Theorem 3.2.1 characterizes ordinal sums by fixed points of the diagonal section. This file proves the version for an arbitrary family J of pairwise disjoint open intervals: a copula C is an ordinal sum with respect to J if and only if δ_C(t) = t for every t ∈ [0,1] outside the open intervals (exists_generalOrdinalSum_iff). In that case the components are unique (existsUnique_generalOrdinalSum_iff) and are the rescaled restrictions

C_k(s,t) = (C(a_k + w_k s, a_k + w_k t) - a_k) / w_k,

which are copulas as soon as δ_C(a_k) = a_k and δ_C(b_k) = b_k (OrdinalIntervals.component). The binary case is exists_ordinalSum_iff_exists_diagonal_fixedPoint in Copula.OrdinalSum.Decomposition.

@[simp]

theorem ProbabilityTheory.Copula.OrdinalIntervals.embed_zero {ι : Type u_1} (J : OrdinalIntervals ι) (k : ι) : J.embed k 0 = J.left k

@[simp]

theorem ProbabilityTheory.Copula.OrdinalIntervals.embed_one {ι : Type u_1} (J : OrdinalIntervals ι) (k : ι) : J.embed k 1 = J.right k

theorem ProbabilityTheory.Copula.OrdinalIntervals.embed_mono {ι : Type u_1} (J : OrdinalIntervals ι) (k : ι) : Monotone (J.embed k)

theorem ProbabilityTheory.Copula.OrdinalIntervals.embed_coord {ι : Type u_1} (J : OrdinalIntervals ι) (k : ι) {u : ↑unitInterval} (hl : J.left k ≤ u) (hr : u ≤ J.right k) : J.embed k (J.coord k u) = u

noncomputable def ProbabilityTheory.Copula.OrdinalIntervals.componentCDF {ι : Type u_1} (J : OrdinalIntervals ι) (C : Copula 2) (k : ι) (s t : ↑unitInterval) : ℝ

The rescaled restriction of C to the square [a_k, b_k]².

Equations

• J.componentCDF C k s t = (C.cdf ![J.embed k s, J.embed k t] - ↑(J.left k)) / J.width k

theorem ProbabilityTheory.Copula.OrdinalIntervals.isClassical_componentCDF {ι : Type u_1} (J : OrdinalIntervals ι) (C : Copula 2) (k : ι) (ha : C.diagonal (J.left k) = ↑(J.left k)) (hb : C.diagonal (J.right k) = ↑(J.right k)) : IsClassical fun (x : Fin 2 → ↑unitInterval) => J.componentCDF C k (x 0) (x 1)

noncomputable def ProbabilityTheory.Copula.OrdinalIntervals.component {ι : Type u_1} (J : OrdinalIntervals ι) (C : Copula 2) (k : ι) (ha : C.diagonal (J.left k) = ↑(J.left k)) (hb : C.diagonal (J.right k) = ↑(J.right k)) : Copula 2

The component of C on the kth square, a copula when both endpoints are diagonal fixed points.

Equations

• J.component C k ha hb = ProbabilityTheory.Copula.ofClassical (fun (x : Fin 2 → ↑unitInterval) => J.componentCDF C k (x 0) (x 1)) ⋯

theorem ProbabilityTheory.Copula.OrdinalIntervals.cdf_component {ι : Type u_1} (J : OrdinalIntervals ι) (C : Copula 2) (k : ι) (ha : C.diagonal (J.left k) = ↑(J.left k)) (hb : C.diagonal (J.right k) = ↑(J.right k)) (s t : ↑unitInterval) : (J.component C k ha hb).cdf ![s, t] = (C.cdf ![J.embed k s, J.embed k t] - ↑(J.left k)) / J.width k

theorem ProbabilityTheory.Copula.OrdinalIntervals.component_generalOrdinalSum {ι : Type u_1} (J : OrdinalIntervals ι) (C : ι → Copula 2) (k : ι) (ha : (generalOrdinalSum J C).diagonal (J.left k) = ↑(J.left k)) (hb : (generalOrdinalSum J C).diagonal (J.right k) = ↑(J.right k)) : J.component (generalOrdinalSum J C) k ha hb = C k

The components of an ordinal sum are its summands.

theorem ProbabilityTheory.Copula.eq_generalOrdinalSum_component {ι : Type u_1} (J : OrdinalIntervals ι) (C : Copula 2) (h : ∀ (t : ↑unitInterval), (∀ (k : ι), ¬(J.left k < t ∧ t < J.right k)) → C.diagonal t = ↑t) : C = generalOrdinalSum J fun (k : ι) => J.component C k ⋯ ⋯

If the diagonal of C is the identity outside the open intervals, then C is the ordinal sum of its components.

theorem ProbabilityTheory.Copula.exists_generalOrdinalSum_iff {ι : Type u_1} (J : OrdinalIntervals ι) (C : Copula 2) : (∃ (D : ι → Copula 2), C = generalOrdinalSum J D) ↔ ∀ (t : ↑unitInterval), (∀ (k : ι), ¬(J.left k < t ∧ t < J.right k)) → C.diagonal t = ↑t

Nelsen, Theorem 3.2.1 (general form): C is an ordinal sum with respect to J if and only if its diagonal is the identity outside the open intervals of J.

theorem ProbabilityTheory.Copula.existsUnique_generalOrdinalSum_iff {ι : Type u_1} (J : OrdinalIntervals ι) (C : Copula 2) : (∃! D : ι → Copula 2, C = generalOrdinalSum J D) ↔ ∀ (t : ↑unitInterval), (∀ (k : ι), ¬(J.left k < t ∧ t < J.right k)) → C.diagonal t = ↑t

The decomposition of Nelsen, Theorem 3.2.1 is unique.