← Copula mathematical handbook

Quasi-copulas

Nelsen, An Introduction to Copulas, second edition, §6.2. Nelsen defines quasi-copulas through tracks; following Genest, Quesada Molina, Rodríguez Lallena and Sempi (1999), who proved the equivalence, and Durante–Sempi, Principles of Copula Theory, §7.2, we use the functional characterization as the definition.

A d-quasi-copula is a function Q : [0,1]^d → ℝ that is grounded, has uniform one-dimensional margins, is nondecreasing in each argument, and satisfies the Lipschitz condition |Q u - Q v| ≤ ∑ i, |u i - v i| (IsQuasiCopula). As for IsClassical, the value at the top corner is required explicitly so that dimension zero is covered.

• Every copula CDF, and more generally every function satisfying the classical copula conditions, is a quasi-copula (isQuasiCopula_cdf, IsClassical.isQuasiCopula); a quasi-copula is a copula exactly when all of its rectangle increments are nonnegative (isClassical_iff_isQuasiCopula).
• Quasi-copulas satisfy the Fréchet–Hoeffding bounds (IsQuasiCopula.frechet_lower_le, IsQuasiCopula.le_frechet_upper, and for d = 2 the forms W ≤ Q ≤ M).
• Pointwise suprema and infima of nonempty families of quasi-copulas, in particular of copulas, are quasi-copulas (IsQuasiCopula.iSup, IsQuasiCopula.iInf), and quasi-copulas are closed under convex combinations (IsQuasiCopula.convexCombination).

The bivariate characterization by rectangles touching the boundary and a proper quasi-copula are in Copula.QuasiCopula.Bivariate.

structure ProbabilityTheory.Copula.IsQuasiCopula {d : ℕ} (Q : (Fin d → ↑unitInterval) → ℝ) : Prop

A d-dimensional quasi-copula: grounded, uniform margins, nondecreasing in each argument, and 1-Lipschitz for the sum of coordinate distances.

• normalized : (Q fun (x : Fin d) => 1) = 1

  The top corner has value one, including in dimension zero.

• grounded (u : Fin d → ↑unitInterval) (i : Fin d) : u i = 0 → Q u = 0

  A zero coordinate makes the function vanish.

• marginal (i : Fin d) (t : ↑unitInterval) : Q (Function.update (fun (x : Fin d) => 1) i t) = ↑t

  The one-coordinate boundary faces are uniform.

• monotone : Monotone Q

  Monotonicity in the pointwise order.

• lipschitz (u v : Fin d → ↑unitInterval) : |Q u - Q v| ≤ ∑ i : Fin d, |↑(u i) - ↑(v i)|

  The Lipschitz condition for the sum of coordinate distances.

theorem ProbabilityTheory.Copula.IsClassical.isQuasiCopula {d : ℕ} {F : (Fin d → ↑unitInterval) → ℝ} (hF : IsClassical F) : IsQuasiCopula F

Functions satisfying the classical copula conditions are quasi-copulas.

theorem ProbabilityTheory.Copula.isQuasiCopula_cdf {d : ℕ} (C : Copula d) : IsQuasiCopula C.cdf

Every copula is a quasi-copula.

theorem ProbabilityTheory.Copula.isClassical_iff_isQuasiCopula {d : ℕ} {F : (Fin d → ↑unitInterval) → ℝ} : IsClassical F ↔ IsQuasiCopula F ∧ ∀ (a b : Fin d → ↑unitInterval), a ≤ b → 0 ≤ rectangleIncrement F a b

A quasi-copula is (the CDF of) a copula exactly when all rectangle increments are nonnegative.

theorem ProbabilityTheory.Copula.cdf_ne_of_rectangleIncrement_neg {d : ℕ} {F : (Fin d → ↑unitInterval) → ℝ} {a b : Fin d → ↑unitInterval} (hab : a ≤ b) (h : rectangleIncrement F a b < 0) (C : Copula d) : C.cdf ≠ F

A quasi-copula with a negative rectangle increment is not the CDF of any copula.

theorem ProbabilityTheory.Copula.IsQuasiCopula.le_coord {d : ℕ} {Q : (Fin d → ↑unitInterval) → ℝ} (hQ : IsQuasiCopula Q) (u : Fin d → ↑unitInterval) (i : Fin d) : Q u ≤ ↑(u i)

theorem ProbabilityTheory.Copula.IsQuasiCopula.le_one {d : ℕ} {Q : (Fin d → ↑unitInterval) → ℝ} (hQ : IsQuasiCopula Q) (u : Fin d → ↑unitInterval) : Q u ≤ 1

theorem ProbabilityTheory.Copula.IsQuasiCopula.nonneg {d : ℕ} {Q : (Fin d → ↑unitInterval) → ℝ} (hQ : IsQuasiCopula Q) (u : Fin d → ↑unitInterval) : 0 ≤ Q u

theorem ProbabilityTheory.Copula.IsQuasiCopula.sum_sub_dim_add_one_le {d : ℕ} {Q : (Fin d → ↑unitInterval) → ℝ} (hQ : IsQuasiCopula Q) (u : Fin d → ↑unitInterval) : ∑ i : Fin d, ↑(u i) - ↑d + 1 ≤ Q u

The untruncated lower Fréchet–Hoeffding bound for quasi-copulas.

theorem ProbabilityTheory.Copula.IsQuasiCopula.frechet_lower_le {d : ℕ} {Q : (Fin d → ↑unitInterval) → ℝ} (hQ : IsQuasiCopula Q) (u : Fin d → ↑unitInterval) : max 0 (∑ i : Fin d, ↑(u i) - ↑d + 1) ≤ Q u

Fréchet–Hoeffding lower bound for quasi-copulas.

theorem ProbabilityTheory.Copula.IsQuasiCopula.le_frechet_upper {d : ℕ} {Q : (Fin d → ↑unitInterval) → ℝ} (hQ : IsQuasiCopula Q) (u : Fin d → ↑unitInterval) : Q u ≤ ↑(⨅ (i : Fin d), u i)

Fréchet–Hoeffding upper bound for quasi-copulas.

theorem ProbabilityTheory.Copula.IsQuasiCopula.le_cdf_comonotonic {d : ℕ} {Q : (Fin d → ↑unitInterval) → ℝ} (hQ : IsQuasiCopula Q) (u : Fin d → ↑unitInterval) : Q u ≤ (comonotonic d).cdf u

The upper bound Q ≤ M, with M the comonotonic copula.

theorem ProbabilityTheory.Copula.IsQuasiCopula.cdf_countermonotonic_le {Q : (Fin 2 → ↑unitInterval) → ℝ} (hQ : IsQuasiCopula Q) (u : Fin 2 → ↑unitInterval) : countermonotonic.cdf u ≤ Q u

The bivariate lower bound W ≤ Q, with W the countermonotonic copula.

theorem ProbabilityTheory.Copula.IsQuasiCopula.bddAbove_range {d : ℕ} {ι : Type u_1} {Q : ι → (Fin d → ↑unitInterval) → ℝ} (hQ : ∀ (k : ι), IsQuasiCopula (Q k)) (u : Fin d → ↑unitInterval) : BddAbove (Set.range fun (k : ι) => Q k u)

theorem ProbabilityTheory.Copula.IsQuasiCopula.bddBelow_range {d : ℕ} {ι : Type u_1} {Q : ι → (Fin d → ↑unitInterval) → ℝ} (hQ : ∀ (k : ι), IsQuasiCopula (Q k)) (u : Fin d → ↑unitInterval) : BddBelow (Set.range fun (k : ι) => Q k u)

theorem ProbabilityTheory.Copula.IsQuasiCopula.iSup {d : ℕ} {ι : Type u_1} [Nonempty ι] {Q : ι → (Fin d → ↑unitInterval) → ℝ} (hQ : ∀ (k : ι), IsQuasiCopula (Q k)) : IsQuasiCopula fun (u : Fin d → ↑unitInterval) => ⨆ (k : ι), Q k u

The pointwise supremum of a nonempty family of quasi-copulas is a quasi-copula.

theorem ProbabilityTheory.Copula.IsQuasiCopula.iInf {d : ℕ} {ι : Type u_1} [Nonempty ι] {Q : ι → (Fin d → ↑unitInterval) → ℝ} (hQ : ∀ (k : ι), IsQuasiCopula (Q k)) : IsQuasiCopula fun (u : Fin d → ↑unitInterval) => ⨅ (k : ι), Q k u

The pointwise infimum of a nonempty family of quasi-copulas is a quasi-copula.

theorem ProbabilityTheory.Copula.IsQuasiCopula.convexCombination {d : ℕ} {Q R : (Fin d → ↑unitInterval) → ℝ} (hQ : IsQuasiCopula Q) (hR : IsQuasiCopula R) {t : ℝ} (ht0 : 0 ≤ t) (ht1 : t ≤ 1) : IsQuasiCopula fun (u : Fin d → ↑unitInterval) => t * Q u + (1 - t) * R u

Quasi-copulas are closed under convex combinations.

theorem ProbabilityTheory.Copula.isQuasiCopula_iSup_cdf {d : ℕ} {ι : Type u_1} [Nonempty ι] (C : ι → Copula d) : IsQuasiCopula fun (u : Fin d → ↑unitInterval) => ⨆ (k : ι), (C k).cdf u

The pointwise supremum of a nonempty family of copula CDFs is a quasi-copula.

theorem ProbabilityTheory.Copula.isQuasiCopula_iInf_cdf {d : ℕ} {ι : Type u_1} [Nonempty ι] (C : ι → Copula d) : IsQuasiCopula fun (u : Fin d → ↑unitInterval) => ⨅ (k : ι), (C k).cdf u

The pointwise infimum of a nonempty family of copula CDFs is a quasi-copula.