← Copula mathematical handbook

General ordinal sums

Nelsen, An Introduction to Copulas, 2nd ed., Definition 3.2.1: let {(a_k, b_k)} be a family of pairwise disjoint open subintervals of [0,1] and let C_k be copulas. The ordinal sum of the C_k with respect to the intervals is the copula

C(u,v) = a_k + (b_k - a_k) C_k((u - a_k)/(b_k - a_k), (v - a_k)/(b_k - a_k))  on [a_k, b_k]²,
C(u,v) = min(u, v)                                                          elsewhere.

The index type is arbitrary (necessarily at most countably many intervals are nonempty, but no countability assumption is needed), so the construction covers finite and countable families and intervals that do not exhaust [0,1].

Construction

Write w_k = b_k - a_k and c_k(u) = clamp((u - a_k)/w_k, 0, 1). The CDF is assembled as

C(u,v) = min(g(u), g(v)) + ∑' k, w_k C_k(c_k(u), c_k(v)),   g(u) = u - ∑' k, w_k c_k(u).

Here g(u) is the Lebesgue measure of [0,u] outside the intervals (the mass that M puts on the residual part of the diagonal). Disjointness enters through the finite estimate ∑_{k ∈ s} |[x,y] ∩ (a_k, b_k)| ≤ y - x, proved with Lebesgue measure; it gives summability of the widths and monotonicity of g. Two-increasingness holds termwise.

Main declarations

• OrdinalIntervals ι: pairwise disjoint nondegenerate open subintervals of [0,1].
• generalOrdinalSum J C, cdf_generalOrdinalSum.
• cdf_generalOrdinalSum_eq_min_sub: C(u,v) = min(u,v) - ∑' k, w_k (M - C_k)(c_k u, c_k v).

structure ProbabilityTheory.Copula.OrdinalIntervals (ι : Type u_1) : Type u_1

A family of pairwise disjoint nonempty open subintervals (left k, right k) of [0,1] (Nelsen, Definition 3.2.1).

• left : ι → ↑unitInterval
• right : ι → ↑unitInterval
• left_lt_right (k : ι) : self.left k < self.right k
• disjoint : Pairwise fun (k l : ι) => self.right k ≤ self.left l ∨ self.right l ≤ self.left k

def ProbabilityTheory.Copula.OrdinalIntervals.width {ι : Type u_1} (J : OrdinalIntervals ι) (k : ι) : ℝ

Length of the kth interval.

Equations

• J.width k = ↑(J.right k) - ↑(J.left k)

theorem ProbabilityTheory.Copula.OrdinalIntervals.width_pos {ι : Type u_1} (J : OrdinalIntervals ι) (k : ι) : 0 < J.width k

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

The clipped affine coordinate of the kth interval.

Equations

• J.coord k u = Set.projIcc 0 1 ProbabilityTheory.Copula.OrdinalIntervals.coord._proof_1 ((↑u - ↑(J.left k)) / J.width k)

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

theorem ProbabilityTheory.Copula.OrdinalIntervals.coord_of_le {ι : Type u_1} (J : OrdinalIntervals ι) (k : ι) {u : ↑unitInterval} (hu : u ≤ J.left k) : J.coord k u = 0

theorem ProbabilityTheory.Copula.OrdinalIntervals.coord_of_ge {ι : Type u_1} (J : OrdinalIntervals ι) (k : ι) {u : ↑unitInterval} (hu : J.right k ≤ u) : J.coord k u = 1

@[simp]

theorem ProbabilityTheory.Copula.OrdinalIntervals.coord_zero {ι : Type u_1} (J : OrdinalIntervals ι) (k : ι) : J.coord k 0 = 0

@[simp]

theorem ProbabilityTheory.Copula.OrdinalIntervals.coord_one {ι : Type u_1} (J : OrdinalIntervals ι) (k : ι) : J.coord k 1 = 1

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

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

On its interval, the coordinate inverts the affine map s ↦ a_k + w_k s.

theorem ProbabilityTheory.Copula.OrdinalIntervals.width_mul_coord {ι : Type u_1} (J : OrdinalIntervals ι) (k : ι) (u : ↑unitInterval) : J.width k * ↑(J.coord k u) = min ↑u ↑(J.right k) - min ↑u ↑(J.left k)

theorem ProbabilityTheory.Copula.OrdinalIntervals.width_mul_coord_nonneg {ι : Type u_1} (J : OrdinalIntervals ι) (k : ι) (u : ↑unitInterval) : 0 ≤ J.width k * ↑(J.coord k u)

theorem ProbabilityTheory.Copula.OrdinalIntervals.width_mul_coord_le {ι : Type u_1} (J : OrdinalIntervals ι) (k : ι) (u : ↑unitInterval) : J.width k * ↑(J.coord k u) ≤ J.width k

Disjointness and summability

theorem ProbabilityTheory.Copula.OrdinalIntervals.sum_inter_le {ι : Type u_1} (J : OrdinalIntervals ι) (s : Finset ι) {x y : ℝ} (hxy : x ≤ y) : ∑ k ∈ s, max (min (↑(J.right k)) y - max (↑(J.left k)) x) 0 ≤ y - x

Finitely many disjoint intervals meet [x, y] in total length at most y - x.

theorem ProbabilityTheory.Copula.OrdinalIntervals.sum_increment_le {ι : Type u_1} (J : OrdinalIntervals ι) (s : Finset ι) {u v : ↑unitInterval} (huv : u ≤ v) : ∑ k ∈ s, (J.width k * ↑(J.coord k v) - J.width k * ↑(J.coord k u)) ≤ ↑v - ↑u

The increments of the weighted coordinates between u ≤ v add up to at most v - u.

theorem ProbabilityTheory.Copula.OrdinalIntervals.increment_nonneg {ι : Type u_1} (J : OrdinalIntervals ι) (k : ι) {u v : ↑unitInterval} (huv : u ≤ v) : 0 ≤ J.width k * ↑(J.coord k v) - J.width k * ↑(J.coord k u)

theorem ProbabilityTheory.Copula.OrdinalIntervals.sum_width_le_one {ι : Type u_1} (J : OrdinalIntervals ι) (s : Finset ι) : ∑ k ∈ s, J.width k ≤ 1

theorem ProbabilityTheory.Copula.OrdinalIntervals.summable_width {ι : Type u_1} (J : OrdinalIntervals ι) : Summable J.width

theorem ProbabilityTheory.Copula.OrdinalIntervals.tsum_width_le_one {ι : Type u_1} (J : OrdinalIntervals ι) : ∑' (k : ι), J.width k ≤ 1

theorem ProbabilityTheory.Copula.OrdinalIntervals.summable_of_abs_le {ι : Type u_1} (J : OrdinalIntervals ι) {f : ι → ℝ} (hf : ∀ (k : ι), |f k| ≤ J.width k) : Summable f

Summability of any family dominated by the widths.

theorem ProbabilityTheory.Copula.OrdinalIntervals.summable_width_mul_coord {ι : Type u_1} (J : OrdinalIntervals ι) (u : ↑unitInterval) : Summable fun (k : ι) => J.width k * ↑(J.coord k u)

The residual diagonal mass

noncomputable def ProbabilityTheory.Copula.OrdinalIntervals.gap {ι : Type u_1} (J : OrdinalIntervals ι) (u : ↑unitInterval) : ℝ

The Lebesgue measure of [0,u] outside the intervals: u - ∑' k, w_k c_k(u).

Equations

• J.gap u = ↑u - ∑' (k : ι), J.width k * ↑(J.coord k u)

theorem ProbabilityTheory.Copula.OrdinalIntervals.gap_mono {ι : Type u_1} (J : OrdinalIntervals ι) : Monotone J.gap

@[simp]

theorem ProbabilityTheory.Copula.OrdinalIntervals.gap_zero {ι : Type u_1} (J : OrdinalIntervals ι) : J.gap 0 = 0

theorem ProbabilityTheory.Copula.OrdinalIntervals.gap_nonneg {ι : Type u_1} (J : OrdinalIntervals ι) (u : ↑unitInterval) : 0 ≤ J.gap u

theorem ProbabilityTheory.Copula.OrdinalIntervals.gap_min {ι : Type u_1} (J : OrdinalIntervals ι) (u v : ↑unitInterval) : J.gap (min u v) = min (J.gap u) (J.gap v)

The general ordinal sum

theorem ProbabilityTheory.Copula.OrdinalIntervals.summable_cdf {ι : Type u_1} (J : OrdinalIntervals ι) (C : ι → Copula 2) (u v : ↑unitInterval) : Summable fun (k : ι) => J.width k * (C k).cdf ![J.coord k u, J.coord k v]

noncomputable def ProbabilityTheory.Copula.OrdinalIntervals.cdf {ι : Type u_1} (J : OrdinalIntervals ι) (C : ι → Copula 2) (u v : ↑unitInterval) : ℝ

The CDF of the ordinal sum.

Equations

• J.cdf C u v = min (J.gap u) (J.gap v) + ∑' (k : ι), J.width k * (C k).cdf ![J.coord k u, J.coord k v]

theorem ProbabilityTheory.Copula.OrdinalIntervals.isClassical {ι : Type u_1} (J : OrdinalIntervals ι) (C : ι → Copula 2) : IsClassical fun (u : Fin 2 → ↑unitInterval) => J.cdf C (u 0) (u 1)

noncomputable def ProbabilityTheory.Copula.generalOrdinalSum {ι : Type u_1} (J : OrdinalIntervals ι) (C : ι → Copula 2) : Copula 2

General ordinal sum (Nelsen, Definition 3.2.1): the copula equal to a_k + w_k C_k((u - a_k)/w_k, (v - a_k)/w_k) on the squares [a_k, b_k]² and to M elsewhere.

Equations

• ProbabilityTheory.Copula.generalOrdinalSum J C = ProbabilityTheory.Copula.ofClassical (fun (u : Fin 2 → ↑unitInterval) => J.cdf C (u 0) (u 1)) ⋯

@[simp]

theorem ProbabilityTheory.Copula.cdf_generalOrdinalSum {ι : Type u_1} (J : OrdinalIntervals ι) (C : ι → Copula 2) (u : Fin 2 → ↑unitInterval) : (generalOrdinalSum J C).cdf u = min (J.gap (u 0)) (J.gap (u 1)) + ∑' (k : ι), J.width k * (C k).cdf ![J.coord k (u 0), J.coord k (u 1)]

theorem ProbabilityTheory.Copula.cdf_generalOrdinalSum_two {ι : Type u_1} (J : OrdinalIntervals ι) (C : ι → Copula 2) (u v : ↑unitInterval) : (generalOrdinalSum J C).cdf ![u, v] = min (J.gap u) (J.gap v) + ∑' (k : ι), J.width k * (C k).cdf ![J.coord k u, J.coord k v]

noncomputable def ProbabilityTheory.Copula.OrdinalIntervals.defect {ι : Type u_1} (J : OrdinalIntervals ι) (C : ι → Copula 2) (k : ι) (u v : ↑unitInterval) : ℝ

The defect of the kth block from M: w_k (M - C_k)(c_k u, c_k v).

Equations

• J.defect C k u v = J.width k * (min ↑(J.coord k u) ↑(J.coord k v) - (C k).cdf ![J.coord k u, J.coord k v])

theorem ProbabilityTheory.Copula.OrdinalIntervals.summable_defect {ι : Type u_1} (J : OrdinalIntervals ι) (C : ι → Copula 2) (u v : ↑unitInterval) : Summable fun (k : ι) => J.defect C k u v

theorem ProbabilityTheory.Copula.cdf_generalOrdinalSum_eq_min_sub {ι : Type u_1} (J : OrdinalIntervals ι) (C : ι → Copula 2) (u v : ↑unitInterval) : (generalOrdinalSum J C).cdf ![u, v] = min ↑u ↑v - ∑' (k : ι), J.defect C k u v

The ordinal sum as M minus the defects of the blocks.