← Copula mathematical handbook

The prescribed-value bounds are copulas

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

For (a, b) ∈ [0,1]² and max (0, a + b - 1) ≤ θ ≤ min (a, b), the upper bound min (u, v, θ + (u - a)⁺ + (v - b)⁺) and the lower bound max (0, u + v - 1, θ - (a - u)⁺ - (b - v)⁺) are copulas taking the value θ at (a, b) (prescribedUpperCopula, prescribedLowerCopula). Together with the bounds of Copula.QuasiCopula.PrescribedValue this shows that they are the pointwise best-possible bounds for copulas, and for quasi-copulas, with C(a, b) = θ (isGreatest_prescribedUpper, isLeast_prescribedLower, isGreatest_prescribedUpper_quasiCopula, isLeast_prescribedLower_quasiCopula).

Real-variable facts

theorem ProbabilityTheory.Copula.prescribedUpper_rectangle_nonneg {a b θ : ℝ} (h0 : 0 ≤ θ) (ha : θ ≤ a) (hb : θ ≤ b) {u₁ u₂ v₁ v₂ : ℝ} (hu₀ : 0 ≤ u₁) (hu : u₁ ≤ u₂) (hu₁ : u₂ ≤ 1) (hv₀ : 0 ≤ v₁) (hv : v₁ ≤ v₂) (hv₁ : v₂ ≤ 1) : 0 ≤ prescribedUpper a b θ u₂ v₂ - prescribedUpper a b θ u₁ v₂ - prescribedUpper a b θ u₂ v₁ + prescribedUpper a b θ u₁ v₁

theorem ProbabilityTheory.Copula.prescribedUpper_zero_left {a b θ t : ℝ} (h0 : 0 ≤ θ) (ha : 0 ≤ a) (ht : 0 ≤ t) : prescribedUpper a b θ 0 t = 0

theorem ProbabilityTheory.Copula.prescribedUpper_zero_right {a b θ s : ℝ} (h0 : 0 ≤ θ) (hb : 0 ≤ b) (hs : 0 ≤ s) : prescribedUpper a b θ s 0 = 0

theorem ProbabilityTheory.Copula.prescribedUpper_one_left {a b θ t : ℝ} (h1 : a + b - 1 ≤ θ) (ht1 : t ≤ 1) : prescribedUpper a b θ 1 t = t

theorem ProbabilityTheory.Copula.prescribedUpper_one_right {a b θ s : ℝ} (h1 : a + b - 1 ≤ θ) (hs1 : s ≤ 1) : prescribedUpper a b θ s 1 = s

theorem ProbabilityTheory.Copula.prescribedUpper_self {a b θ : ℝ} (ha : θ ≤ a) (hb : θ ≤ b) : prescribedUpper a b θ a b = θ

theorem ProbabilityTheory.Copula.prescribedLower_self {a b θ : ℝ} (h0 : 0 ≤ θ) (h1 : a + b - 1 ≤ θ) : prescribedLower a b θ a b = θ

theorem ProbabilityTheory.Copula.sub_prescribedUpper_reflect (a b θ u v : ℝ) : u - prescribedUpper a (1 - b) (a - θ) u (1 - v) = prescribedLower a b θ u v

Reflecting the second coordinate of the upper bound for (a, 1 - b, a - θ) gives the lower bound for (a, b, θ).

The copulas

theorem ProbabilityTheory.Copula.isClassical_prescribedUpper (a b : ↑unitInterval) {θ : ℝ} (h0 : 0 ≤ θ) (h1 : ↑a + ↑b - 1 ≤ θ) (ha : θ ≤ ↑a) (hb : θ ≤ ↑b) : IsClassical fun (u : Fin 2 → ↑unitInterval) => prescribedUpper (↑a) (↑b) θ ↑(u 0) ↑(u 1)

noncomputable def ProbabilityTheory.Copula.prescribedUpperCopula (a b : ↑unitInterval) {θ : ℝ} (h0 : 0 ≤ θ) (h1 : ↑a + ↑b - 1 ≤ θ) (ha : θ ≤ ↑a) (hb : θ ≤ ↑b) : Copula 2

The upper Fréchet-type bound for a prescribed value C(a, b) = θ, as a copula (a shuffle of M).

Equations

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

theorem ProbabilityTheory.Copula.cdf_prescribedUpperCopula (a b : ↑unitInterval) {θ : ℝ} (h0 : 0 ≤ θ) (h1 : ↑a + ↑b - 1 ≤ θ) (ha : θ ≤ ↑a) (hb : θ ≤ ↑b) (u v : ↑unitInterval) : (prescribedUpperCopula a b h0 h1 ha hb).cdf ![u, v] = prescribedUpper (↑a) (↑b) θ ↑u ↑v

theorem ProbabilityTheory.Copula.cdf_prescribedUpperCopula_self (a b : ↑unitInterval) {θ : ℝ} (h0 : 0 ≤ θ) (h1 : ↑a + ↑b - 1 ≤ θ) (ha : θ ≤ ↑a) (hb : θ ≤ ↑b) : (prescribedUpperCopula a b h0 h1 ha hb).cdf ![a, b] = θ

noncomputable def ProbabilityTheory.Copula.prescribedLowerCopula (a b : ↑unitInterval) {θ : ℝ} (h0 : 0 ≤ θ) (h1 : ↑a + ↑b - 1 ≤ θ) (ha : θ ≤ ↑a) (hb : θ ≤ ↑b) : Copula 2

The lower Fréchet-type bound for a prescribed value C(a, b) = θ, as a copula: the reflection in the second coordinate of the upper bound for C(a, 1 - b) = a - θ.

Equations

• ProbabilityTheory.Copula.prescribedLowerCopula a b h0 h1 ha hb = (ProbabilityTheory.Copula.prescribedUpperCopula a (unitInterval.symm b) ⋯ ⋯ ⋯ ⋯).reflect {1}

theorem ProbabilityTheory.Copula.cdf_prescribedLowerCopula (a b : ↑unitInterval) {θ : ℝ} (h0 : 0 ≤ θ) (h1 : ↑a + ↑b - 1 ≤ θ) (ha : θ ≤ ↑a) (hb : θ ≤ ↑b) (u v : ↑unitInterval) : (prescribedLowerCopula a b h0 h1 ha hb).cdf ![u, v] = prescribedLower (↑a) (↑b) θ ↑u ↑v

theorem ProbabilityTheory.Copula.cdf_prescribedLowerCopula_self (a b : ↑unitInterval) {θ : ℝ} (h0 : 0 ≤ θ) (h1 : ↑a + ↑b - 1 ≤ θ) (ha : θ ≤ ↑a) (hb : θ ≤ ↑b) : (prescribedLowerCopula a b h0 h1 ha hb).cdf ![a, b] = θ

Best-possible bounds

theorem ProbabilityTheory.Copula.isGreatest_prescribedUpper (a b : ↑unitInterval) {θ : ℝ} (h0 : 0 ≤ θ) (h1 : ↑a + ↑b - 1 ≤ θ) (ha : θ ≤ ↑a) (hb : θ ≤ ↑b) (u v : ↑unitInterval) : IsGreatest {x : ℝ | ∃ (C : Copula 2), C.cdf ![a, b] = θ ∧ C.cdf ![u, v] = x} (prescribedUpper (↑a) (↑b) θ ↑u ↑v)

Nelsen, Theorem 3.2.3 (upper bound is best possible). Among copulas with C(a, b) = θ, the largest possible value of C(u, v) is min (u, v, θ + (u - a)⁺ + (v - b)⁺).

theorem ProbabilityTheory.Copula.isLeast_prescribedLower (a b : ↑unitInterval) {θ : ℝ} (h0 : 0 ≤ θ) (h1 : ↑a + ↑b - 1 ≤ θ) (ha : θ ≤ ↑a) (hb : θ ≤ ↑b) (u v : ↑unitInterval) : IsLeast {x : ℝ | ∃ (C : Copula 2), C.cdf ![a, b] = θ ∧ C.cdf ![u, v] = x} (prescribedLower (↑a) (↑b) θ ↑u ↑v)

Nelsen, Theorem 3.2.3 (lower bound is best possible). Among copulas with C(a, b) = θ, the smallest possible value of C(u, v) is max (0, u + v - 1, θ - (a - u)⁺ - (b - v)⁺).

theorem ProbabilityTheory.Copula.isGreatest_prescribedUpper_quasiCopula (a b : ↑unitInterval) {θ : ℝ} (h0 : 0 ≤ θ) (h1 : ↑a + ↑b - 1 ≤ θ) (ha : θ ≤ ↑a) (hb : θ ≤ ↑b) (u v : ↑unitInterval) : IsGreatest {x : ℝ | ∃ (Q : (Fin 2 → ↑unitInterval) → ℝ), IsQuasiCopula Q ∧ Q ![a, b] = θ ∧ Q ![u, v] = x} (prescribedUpper (↑a) (↑b) θ ↑u ↑v)

The upper bound is also best possible among quasi-copulas with Q(a, b) = θ.

theorem ProbabilityTheory.Copula.isLeast_prescribedLower_quasiCopula (a b : ↑unitInterval) {θ : ℝ} (h0 : 0 ≤ θ) (h1 : ↑a + ↑b - 1 ≤ θ) (ha : θ ≤ ↑a) (hb : θ ≤ ↑b) (u v : ↑unitInterval) : IsLeast {x : ℝ | ∃ (Q : (Fin 2 → ↑unitInterval) → ℝ), IsQuasiCopula Q ∧ Q ![a, b] = θ ∧ Q ![u, v] = x} (prescribedLower (↑a) (↑b) θ ↑u ↑v)

The lower bound is also best possible among quasi-copulas with Q(a, b) = θ.