Bivariate quasi-copulas #

Nelsen, An Introduction to Copulas, second edition, §6.2.

IsQuasiCopula.ofBivariate checks the quasi-copula conditions for a two-variable formula from the four boundary identities, monotonicity and the one-sided Lipschitz bounds in each variable.
Characterization of Genest, Quesada Molina, Rodríguez Lallena and Sempi (1999) (Nelsen, §6.2): a function on [0,1]² with the copula boundary conditions is a quasi-copula if and only if every rectangle with at least one side on the boundary of the unit square has a nonnegative increment (isQuasiCopula_iff_rectangleIncrement_nonneg_of_boundary). A copula needs this for every rectangle.
A proper quasi-copula (quasiCopulaExample): the function Q(u,v) = max (W(u,v), min (u, v, max(u,v) - 1/3)), which spreads mass 1/3 uniformly on each of the segments from (0,1/3) to (1/3,2/3), (1/3,0) to (2/3,1/3), (1/3,2/3) to (2/3,1) and (2/3,1/3) to (1,2/3), and mass -1/3 on the diagonal segment from (1/3,1/3) to (2/3,2/3); cf. the proper quasi-copulas in Nelsen, §6.2. The rectangle [1/3,2/3]² has increment -1/3, so it is not a copula (not_isClassical_quasiCopulaExample).

source

theorem ProbabilityTheory.Copula.eq_vecCons_two (u : Fin 2 → ↑unitInterval) :

u = ![u 0, u 1]

source

theorem ProbabilityTheory.Copula.update_one_zero (t : ↑unitInterval) :

Function.update (fun (x : Fin 2) => 1) 0 t = ![t, 1]

source

theorem ProbabilityTheory.Copula.update_one_one (t : ↑unitInterval) :

Function.update (fun (x : Fin 2) => 1) 1 t = ![1, t]

source

theorem ProbabilityTheory.Copula.IsQuasiCopula.ofBivariate (F : ↑unitInterval → ↑unitInterval → ℝ) (hz₁ : ∀ (v : ↑unitInterval), F 0 v = 0) (hz₂ : ∀ (u : ↑unitInterval), F u 0 = 0) (ho₁ : ∀ (v : ↑unitInterval), F 1 v = ↑v) (ho₂ : ∀ (u : ↑unitInterval), F u 1 = ↑u) (hm₁ : ∀ (u u' v : ↑unitInterval), u ≤ u' → F u v ≤ F u' v) (hm₂ : ∀ (u v v' : ↑unitInterval), v ≤ v' → F u v ≤ F u v') (hl₁ : ∀ (u u' v : ↑unitInterval), u ≤ u' → F u' v - F u v ≤ ↑u' - ↑u) (hl₂ : ∀ (u v v' : ↑unitInterval), v ≤ v' → F u v' - F u v ≤ ↑v' - ↑v) :

IsQuasiCopula fun (u : Fin 2 → ↑unitInterval) => F (u 0) (u 1)

Check the quasi-copula conditions for a bivariate formula: the four boundary identities, monotonicity in each variable, and the Lipschitz bound in each variable.

source

theorem ProbabilityTheory.Copula.isQuasiCopula_iff_rectangleIncrement_nonneg_of_boundary {Q : (Fin 2 → ↑unitInterval) → ℝ} :

IsQuasiCopula Q ↔ (∀ (u : Fin 2 → ↑unitInterval) (i : Fin 2), u i = 0 → Q u = 0) ∧ (∀ (i : Fin 2) (t : ↑unitInterval), Q (Function.update (fun (x : Fin 2) => 1) i t) = ↑t) ∧ ∀ (a b : Fin 2 → ↑unitInterval), a ≤ b → (∃ (i : Fin 2), a i = 0 ∨ b i = 1) → 0 ≤ rectangleIncrement Q a b

Characterization of bivariate quasi-copulas (Genest, Quesada Molina, Rodríguez Lallena and Sempi, 1999). A function on [0,1]² is a quasi-copula if and only if it satisfies the copula boundary conditions and every rectangle with a side on the boundary of the unit square has a nonnegative increment.