← Copula mathematical handbook

Best-possible bounds for copulas with a prescribed value

Nelsen, An Introduction to Copulas, second edition, Theorem 3.2.3, and its quasi-copula version in §6.2.

If a bivariate copula (or quasi-copula) C takes the value θ at the point (a, b), then for all (u, v)

max (0, u + v - 1, θ - (a - u)⁺ - (b - v)⁺) ≤ C(u, v) ≤ min (u, v, θ + (u - a)⁺ + (v - b)⁺)

(IsQuasiCopula.prescribedLower_le, IsQuasiCopula.le_prescribedUpper and the copula versions prescribedLower_le_cdf, cdf_le_prescribedUpper). Both bounds are copulas taking the value θ at (a, b) whenever W(a,b) ≤ θ ≤ M(a,b) (prescribedUpperCopula, prescribedLowerCopula), so they are pointwise best-possible, even among quasi-copulas (isGreatest_prescribedUpper, isLeast_prescribedLower and their quasi-copula versions).

The upper bound is the shuffle of M that moves the strips [θ, a] and [a, a + b - θ] of the first coordinate onto [b, a + b - θ] and [θ, b]; this representation (prescribedUpper_eq_shuffle) gives the rectangle inequality. The lower bound is obtained from the upper bound for the parameters (a, 1 - b, a - θ) by reflecting the second coordinate.

noncomputable def ProbabilityTheory.Copula.prescribedUpper (a b θ u v : ℝ) : ℝ

Nelsen's upper bound min (u, v, θ + (u - a)⁺ + (v - b)⁺) for copulas with C(a, b) = θ.

Equations

• ProbabilityTheory.Copula.prescribedUpper a b θ u v = min (min u v) (θ + max (u - a) 0 + max (v - b) 0)

noncomputable def ProbabilityTheory.Copula.prescribedLower (a b θ u v : ℝ) : ℝ

Nelsen's lower bound max (0, u + v - 1, θ - (a - u)⁺ - (b - v)⁺) for copulas with C(a, b) = θ.

Equations

• ProbabilityTheory.Copula.prescribedLower a b θ u v = max (max 0 (u + v - 1)) (θ - max (a - u) 0 - max (b - v) 0)

theorem ProbabilityTheory.Copula.abs_max_sub_right (x y : ℝ) : |max x y - y| = max (x - y) 0

theorem ProbabilityTheory.Copula.abs_sub_min_right (x y : ℝ) : |y - min x y| = max (y - x) 0

theorem ProbabilityTheory.Copula.coe_max_unitInterval (x y : ↑unitInterval) : ↑(max x y) = max ↑x ↑y

theorem ProbabilityTheory.Copula.coe_min_unitInterval (x y : ↑unitInterval) : ↑(min x y) = min ↑x ↑y

theorem ProbabilityTheory.Copula.IsQuasiCopula.le_prescribedUpper {Q : (Fin 2 → ↑unitInterval) → ℝ} (hQ : IsQuasiCopula Q) (a b u v : ↑unitInterval) : Q ![u, v] ≤ prescribedUpper (↑a) (↑b) (Q ![a, b]) ↑u ↑v

Upper bound for a prescribed value (quasi-copulas).

theorem ProbabilityTheory.Copula.IsQuasiCopula.prescribedLower_le {Q : (Fin 2 → ↑unitInterval) → ℝ} (hQ : IsQuasiCopula Q) (a b u v : ↑unitInterval) : prescribedLower (↑a) (↑b) (Q ![a, b]) ↑u ↑v ≤ Q ![u, v]

Lower bound for a prescribed value (quasi-copulas).

theorem ProbabilityTheory.Copula.cdf_le_prescribedUpper (C : Copula 2) (a b u v : ↑unitInterval) : C.cdf ![u, v] ≤ prescribedUpper (↑a) (↑b) (C.cdf ![a, b]) ↑u ↑v

Nelsen, Theorem 3.2.3 (upper bound).

theorem ProbabilityTheory.Copula.prescribedLower_le_cdf (C : Copula 2) (a b u v : ↑unitInterval) : prescribedLower (↑a) (↑b) (C.cdf ![a, b]) ↑u ↑v ≤ C.cdf ![u, v]

Nelsen, Theorem 3.2.3 (lower bound).

The upper bound is a shuffle of M

noncomputable def ProbabilityTheory.Copula.segmentMass (p w x : ℝ) : ℝ

The length of [p, p + w] ∩ (-∞, x], for w ≥ 0.

Equations

• ProbabilityTheory.Copula.segmentMass p w x = max 0 (min (x - p) w)

theorem ProbabilityTheory.Copula.segmentMass_of_le (p w x : ℝ) (h : x ≤ p) : segmentMass p w x = 0

theorem ProbabilityTheory.Copula.segmentMass_of_mem (p w x : ℝ) (h₁ : p ≤ x) (h₂ : x ≤ p + w) : segmentMass p w x = x - p

theorem ProbabilityTheory.Copula.segmentMass_of_ge (p w x : ℝ) (hw : 0 ≤ w) (h : p + w ≤ x) : segmentMass p w x = w

theorem ProbabilityTheory.Copula.monotone_segmentMass (p w : ℝ) : Monotone (segmentMass p w)

theorem ProbabilityTheory.Copula.min_rectangle_nonneg {x₁ x₂ y₁ y₂ : ℝ} (hx : x₁ ≤ x₂) (hy : y₁ ≤ y₂) : 0 ≤ min x₂ y₂ - min x₁ y₂ - min x₂ y₁ + min x₁ y₁

noncomputable def ProbabilityTheory.Copula.prescribedUpperShuffle (a b θ u v : ℝ) : ℝ

The shuffle of M with strips [0, θ] → [0, θ], [θ, a] → [b, a + b - θ], [a, a + b - θ] → [θ, b] and [a + b - θ, 1] → [a + b - θ, 1].

Equations

• One or more equations did not get rendered due to their size.

theorem ProbabilityTheory.Copula.prescribedUpper_eq_shuffle {a b θ u v : ℝ} (h0 : 0 ≤ θ) (ha : θ ≤ a) (hb : θ ≤ b) (hu0 : 0 ≤ u) (hu1 : u ≤ 1) (hv0 : 0 ≤ v) (hv1 : v ≤ 1) : prescribedUpper a b θ u v = prescribedUpperShuffle a b θ u v

The upper bound agrees with the shuffle of M on the unit square.