← Copula mathematical handbook

Properties of general ordinal sums

For the general ordinal sum generalOrdinalSum J C of Nelsen, An Introduction to Copulas, 2nd ed., Definition 3.2.1, this file proves:

• the defining formula: C(u,v) = a_k + w_k C_k(c_k u, c_k v) on the closed square [a_k, b_k]² (cdf_generalOrdinalSum_of_mem) and C(u,v) = min(u,v) whenever (u,v) lies in none of the open squares (cdf_generalOrdinalSum_of_not_mem);
• recovery of the components (cdf_generalOrdinalSum_embed) and injectivity in the components;
• diagonal fixed points: δ(t) = t outside the open intervals, in particular at all endpoints (the easy half of Nelsen, Theorem 3.2.1);
• transpose and exchangeability, pointwise order, and positive quadrant dependence, extending the binary results of Copula.OrdinalSum.Properties and Copula.OrdinalSum.Dependence;
• the existing constructions as instances: finite ordinal sums on an IntervalPartition (generalOrdinalSum_ofPartition), countable ordinal sums on a CountableIntervalPartition (generalOrdinalSum_ofCountable) and the binary ordinalSum (ordinalSum_eq_generalOrdinalSum).

theorem ProbabilityTheory.Copula.OrdinalIntervals.defect_eq_zero_of_not_mem {ι : Type u_1} (J : OrdinalIntervals ι) (C : ι → Copula 2) (k : ι) (u v : ↑unitInterval) (h : ¬(J.left k < u ∧ u < J.right k ∧ J.left k < v ∧ v < J.right k)) : J.defect C k u v = 0

The kth block does not contribute outside its open square.

theorem ProbabilityTheory.Copula.OrdinalIntervals.not_mem_of_mem_Icc {ι : Type u_1} (J : OrdinalIntervals ι) {k l : ι} (hkl : l ≠ k) {u : ↑unitInterval} (hl : J.left k ≤ u) (hr : u ≤ J.right k) : ¬(J.left l < u ∧ u < J.right l)

A point of a closed square [a_k, b_k] lies in no other open interval.

theorem ProbabilityTheory.Copula.OrdinalIntervals.left_not_mem {ι : Type u_1} (J : OrdinalIntervals ι) (k l : ι) : ¬(J.left l < J.left k ∧ J.left k < J.right l)

The left endpoint of an interval lies in no open interval of the family.

theorem ProbabilityTheory.Copula.OrdinalIntervals.right_not_mem {ι : Type u_1} (J : OrdinalIntervals ι) (k l : ι) : ¬(J.left l < J.right k ∧ J.right k < J.right l)

The right endpoint of an interval lies in no open interval of the family.

noncomputable def ProbabilityTheory.Copula.OrdinalIntervals.embed {ι : Type u_1} (J : OrdinalIntervals ι) (k : ι) (s : ↑unitInterval) : ↑unitInterval

The affine embedding s ↦ a_k + w_k s of [0,1] onto [a_k, b_k].

Equations

• J.embed k s = ⟨↑(J.left k) + J.width k * ↑s, ⋯⟩

theorem ProbabilityTheory.Copula.OrdinalIntervals.coe_embed {ι : Type u_1} (J : OrdinalIntervals ι) (k : ι) (s : ↑unitInterval) : ↑(J.embed k s) = ↑(J.left k) + J.width k * ↑s

theorem ProbabilityTheory.Copula.OrdinalIntervals.left_le_embed {ι : Type u_1} (J : OrdinalIntervals ι) (k : ι) (s : ↑unitInterval) : J.left k ≤ J.embed k s

theorem ProbabilityTheory.Copula.OrdinalIntervals.embed_le_right {ι : Type u_1} (J : OrdinalIntervals ι) (k : ι) (s : ↑unitInterval) : J.embed k s ≤ J.right k

@[simp]

theorem ProbabilityTheory.Copula.OrdinalIntervals.coord_embed {ι : Type u_1} (J : OrdinalIntervals ι) (k : ι) (s : ↑unitInterval) : J.coord k (J.embed k s) = s

The defining formula

theorem ProbabilityTheory.Copula.cdf_generalOrdinalSum_of_not_mem {ι : Type u_1} (J : OrdinalIntervals ι) (C : ι → Copula 2) (u v : ↑unitInterval) (h : ∀ (k : ι), ¬(J.left k < u ∧ u < J.right k ∧ J.left k < v ∧ v < J.right k)) : (generalOrdinalSum J C).cdf ![u, v] = min ↑u ↑v

Off the open squares the ordinal sum coincides with M.

theorem ProbabilityTheory.Copula.cdf_generalOrdinalSum_of_mem {ι : Type u_1} (J : OrdinalIntervals ι) (C : ι → Copula 2) (k : ι) {u v : ↑unitInterval} (hu : J.left k ≤ u ∧ u ≤ J.right k) (hv : J.left k ≤ v ∧ v ≤ J.right k) : (generalOrdinalSum J C).cdf ![u, v] = ↑(J.left k) + J.width k * (C k).cdf ![J.coord k u, J.coord k v]

Nelsen, Definition 3.2.1: on the square [a_k, b_k]² the ordinal sum is a_k + w_k C_k((u - a_k)/w_k, (v - a_k)/w_k).

theorem ProbabilityTheory.Copula.cdf_generalOrdinalSum_embed {ι : Type u_1} (J : OrdinalIntervals ι) (C : ι → Copula 2) (k : ι) (s t : ↑unitInterval) : (generalOrdinalSum J C).cdf ![J.embed k s, J.embed k t] = ↑(J.left k) + J.width k * (C k).cdf ![s, t]

The components are recovered by the affine embedding of their square.

theorem ProbabilityTheory.Copula.cdf_component_eq {ι : Type u_1} (J : OrdinalIntervals ι) (C : ι → Copula 2) (k : ι) (s t : ↑unitInterval) : (C k).cdf ![s, t] = ((generalOrdinalSum J C).cdf ![J.embed k s, J.embed k t] - ↑(J.left k)) / J.width k

theorem ProbabilityTheory.Copula.generalOrdinalSum_injective {ι : Type u_1} (J : OrdinalIntervals ι) : Function.Injective (generalOrdinalSum J)

The general ordinal sum determines its components.

theorem ProbabilityTheory.Copula.generalOrdinalSum_eq_iff {ι : Type u_1} (J : OrdinalIntervals ι) (C D : ι → Copula 2) : generalOrdinalSum J C = generalOrdinalSum J D ↔ C = D

Diagonal fixed points

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

Outside the open intervals the diagonal of an ordinal sum is the identity.

theorem ProbabilityTheory.Copula.diagonal_generalOrdinalSum_left {ι : Type u_1} (J : OrdinalIntervals ι) (C : ι → Copula 2) (k : ι) : (generalOrdinalSum J C).diagonal (J.left k) = ↑(J.left k)

theorem ProbabilityTheory.Copula.diagonal_generalOrdinalSum_right {ι : Type u_1} (J : OrdinalIntervals ι) (C : ι → Copula 2) (k : ι) : (generalOrdinalSum J C).diagonal (J.right k) = ↑(J.right k)

theorem ProbabilityTheory.Copula.diagonal_generalOrdinalSum_of_mem {ι : Type u_1} (J : OrdinalIntervals ι) (C : ι → Copula 2) (k : ι) {t : ↑unitInterval} (ht : J.left k ≤ t ∧ t ≤ J.right k) : (generalOrdinalSum J C).diagonal t = ↑(J.left k) + J.width k * (C k).diagonal (J.coord k t)

Inside a square the diagonal is the rescaled diagonal of the component.

Transpose, order and dependence

theorem ProbabilityTheory.Copula.transpose_generalOrdinalSum {ι : Type u_1} (J : OrdinalIntervals ι) (C : ι → Copula 2) : (generalOrdinalSum J C).transpose = generalOrdinalSum J fun (k : ι) => (C k).transpose

theorem ProbabilityTheory.Copula.IsExchangeable.generalOrdinalSum {ι : Type u_1} (J : OrdinalIntervals ι) (C : ι → Copula 2) (h : ∀ (k : ι), (C k).IsExchangeable) : (Copula.generalOrdinalSum J C).IsExchangeable

theorem ProbabilityTheory.Copula.isExchangeable_generalOrdinalSum_iff {ι : Type u_1} (J : OrdinalIntervals ι) (C : ι → Copula 2) : (generalOrdinalSum J C).IsExchangeable ↔ ∀ (k : ι), (C k).IsExchangeable

An ordinal sum is exchangeable exactly when all components are.

theorem ProbabilityTheory.Copula.lowerOrthantLE_generalOrdinalSum_iff {ι : Type u_1} (J : OrdinalIntervals ι) (C D : ι → Copula 2) : (generalOrdinalSum J C).LowerOrthantLE (generalOrdinalSum J D) ↔ ∀ (k : ι), (C k).LowerOrthantLE (D k)

The ordinal sum is monotone in the components for the pointwise order, and conversely.

theorem ProbabilityTheory.Copula.IsPQD.generalOrdinalSum {ι : Type u_1} (J : OrdinalIntervals ι) (C : ι → Copula 2) (h : ∀ (k : ι), (C k).IsPQD) : (Copula.generalOrdinalSum J C).IsPQD

An ordinal sum of positively quadrant dependent copulas is positively quadrant dependent.

Special cases

@[simp]

theorem ProbabilityTheory.Copula.generalOrdinalSum_comonotonic {ι : Type u_1} (J : OrdinalIntervals ι) : (generalOrdinalSum J fun (x : ι) => comonotonic 2) = comonotonic 2

The ordinal sum of copies of M is M.

theorem ProbabilityTheory.Copula.generalOrdinalSum_of_isEmpty {ι : Type u_1} (J : OrdinalIntervals ι) (C : ι → Copula 2) [IsEmpty ι] : generalOrdinalSum J C = comonotonic 2

The ordinal sum over an empty family of intervals is M.

def ProbabilityTheory.Copula.OrdinalIntervals.ofPartition {n : ℕ} (P : IntervalPartition n) : OrdinalIntervals (Fin n)

The cells of a finite interval partition.

Equations

• ProbabilityTheory.Copula.OrdinalIntervals.ofPartition P = { left := fun (i : Fin n) => P.point i.castSucc, right := fun (i : Fin n) => P.point i.succ, left_lt_right := ⋯, disjoint := ⋯ }

def ProbabilityTheory.Copula.OrdinalIntervals.ofCountable (P : CountableIntervalPartition) : OrdinalIntervals ℕ

The blocks of a countable interval partition.

Equations

• ProbabilityTheory.Copula.OrdinalIntervals.ofCountable P = { left := fun (k : ℕ) => P.point k, right := fun (k : ℕ) => P.point (k + 1), left_lt_right := ⋯, disjoint := ⋯ }

theorem ProbabilityTheory.Copula.generalOrdinalSum_ofPartition {n : ℕ} (P : IntervalPartition n) (C : Fin n → Copula 2) : generalOrdinalSum (OrdinalIntervals.ofPartition P) C = finiteOrdinalSum P C

Finite ordinal sums on an interval partition are general ordinal sums without gaps.

theorem ProbabilityTheory.Copula.generalOrdinalSum_ofCountable (P : CountableIntervalPartition) (C : ℕ → Copula 2) : generalOrdinalSum (OrdinalIntervals.ofCountable P) C = countableOrdinalSum P C

Countable ordinal sums on adjacent blocks are general ordinal sums without gaps.

theorem ProbabilityTheory.Copula.ordinalSum_eq_generalOrdinalSum (C D : Copula 2) (a : ↑unitInterval) (ha0 : 0 < a) (ha1 : a < 1) : C.ordinalSum D a = generalOrdinalSum (OrdinalIntervals.ofPartition (IntervalPartition.binary a ha0 ha1)) ![C, D]

The binary ordinal sum is a general ordinal sum over two intervals.