← Copula mathematical handbook

Upper bounds for copulas and quasi-copulas with a prescribed diagonal

Let δ be a diagonal function and δ̂ t = t - δ t its gap (diagGap). Every copula, and more generally every bivariate quasi-copula Q, with diagonal section δ satisfies Q(u,v) ≤ δ(t) + (u - t)⁺ + (v - t)⁺ for all t, by monotonicity and the Lipschitz property. Taking the infimum gives the bound

A_δ(u,v) = min(u, v, max(u,v) - max_{t ∈ [u ∧ v, u ∨ v]} (t - δ t))

of Nelsen, Quesada-Molina, Rodríguez-Lallena and Úbeda-Flores (Best-possible bounds on sets of bivariate distribution functions, J. Multivariate Anal. 2004); see also Nelsen, An Introduction to Copulas, 2nd ed., §3.2.6 and §6.2.

• diagonalUpperBound δ: defined as min(u, v, inf_t (δ t + (u - t)⁺ + (v - t)⁺)); diagonalUpperBound_eq proves the max-formula above.
• quasiCopula_le_diagonalUpperBound, cdf_le_diagonalUpperBound: Q ≤ A_δ and C ≤ A_δ.
• isQuasiCopula_diagonalUpperBound, diagonalUpperBound_self: A_δ is itself a quasi-copula with diagonal δ; hence (diagonalUpperBound_isGreatest) it is the largest quasi-copula with diagonal δ, the best-possible upper bound on the set of quasi-copulas with diagonal δ.
• bertino_le_cdf_le_upper: B_δ ≤ C ≤ A_δ for copulas with diagonal δ.
• For copulas the bound A_δ need not be best possible: cdf_le_diagonal_add_diagonal_sub_bertino gives the additional bound C(u,v) ≤ δ(u) + δ(v) - B_δ(u,v), and dipDiagonal is an explicit diagonal (δ(t) = t - min(t, 1 - t, 1/10 + |t - 1/2|)) for which every copula C with that diagonal satisfies C(3/10, 7/10) ≤ 1/5 < 3/10 = A_δ(3/10, 7/10) (dipDiagonal_gap). The sup of the copulas with diagonal δ is therefore in general strictly smaller than A_δ (compare Úbeda-Flores, On the best-possible upper bound on sets of copulas with given diagonal sections, Soft Computing 2008).

Bivariate quasi-copulas: monotonicity and Lipschitz bounds in one variable

theorem ProbabilityTheory.Copula.IsQuasiCopula.mono_two {Q : (Fin 2 → ↑unitInterval) → ℝ} (hQ : IsQuasiCopula Q) {u u' v v' : ↑unitInterval} (hu : u ≤ u') (hv : v ≤ v') : Q ![u, v] ≤ Q ![u', v']

theorem ProbabilityTheory.Copula.IsQuasiCopula.sub_le_left {Q : (Fin 2 → ↑unitInterval) → ℝ} (hQ : IsQuasiCopula Q) {s t : ↑unitInterval} (hst : s ≤ t) (v : ↑unitInterval) : Q ![t, v] - Q ![s, v] ≤ ↑t - ↑s

theorem ProbabilityTheory.Copula.IsQuasiCopula.sub_le_right {Q : (Fin 2 → ↑unitInterval) → ℝ} (hQ : IsQuasiCopula Q) {s t : ↑unitInterval} (hst : s ≤ t) (u : ↑unitInterval) : Q ![u, t] - Q ![u, s] ≤ ↑t - ↑s

The upper bound A_δ of Nelsen, Quesada-Molina, Rodríguez-Lallena and Úbeda-Flores

def ProbabilityTheory.Copula.diagUpperAux (δ : ↑unitInterval → ℝ) (t u v : ↑unitInterval) : ℝ

The function δ t + (u - t)⁺ + (v - t)⁺, an upper bound for C(u,v) obtained from the diagonal value at t and the Lipschitz property.

Equations

• ProbabilityTheory.Copula.diagUpperAux δ t u v = δ t + max (↑u - ↑t) 0 + max (↑v - ↑t) 0

noncomputable def ProbabilityTheory.Copula.diagUpperInf (δ : ↑unitInterval → ℝ) (u v : ↑unitInterval) : ℝ

The infimum over t of δ t + (u - t)⁺ + (v - t)⁺.

Equations

• ProbabilityTheory.Copula.diagUpperInf δ u v = ⨅ (t : ↑unitInterval), ProbabilityTheory.Copula.diagUpperAux δ t u v

noncomputable def ProbabilityTheory.Copula.diagonalUpperBound (δ : ↑unitInterval → ℝ) (u v : ↑unitInterval) : ℝ

The upper bound A_δ(u,v) = min(u, v, inf_t (δ t + (u - t)⁺ + (v - t)⁺)) for copulas with diagonal δ; see diagonalUpperBound_eq for the form min(u, v, max(u,v) - max_{t ∈ [u ∧ v, u ∨ v]} (t - δ t)).

Equations

• ProbabilityTheory.Copula.diagonalUpperBound δ u v = min (min ↑u ↑v) (ProbabilityTheory.Copula.diagUpperInf δ u v)

theorem ProbabilityTheory.Copula.diagUpperAux_comm {δ : ↑unitInterval → ℝ} (t u v : ↑unitInterval) : diagUpperAux δ t u v = diagUpperAux δ t v u

theorem ProbabilityTheory.Copula.diagUpperInf_comm {δ : ↑unitInterval → ℝ} (u v : ↑unitInterval) : diagUpperInf δ u v = diagUpperInf δ v u

theorem ProbabilityTheory.Copula.diagonalUpperBound_comm {δ : ↑unitInterval → ℝ} (u v : ↑unitInterval) : diagonalUpperBound δ u v = diagonalUpperBound δ v u

theorem ProbabilityTheory.Copula.IsDiagonalFunction.diagUpperAux_nonneg {δ : ↑unitInterval → ℝ} (hδ : IsDiagonalFunction δ) (t u v : ↑unitInterval) : 0 ≤ diagUpperAux δ t u v

theorem ProbabilityTheory.Copula.IsDiagonalFunction.bddBelow_diagUpperAux {δ : ↑unitInterval → ℝ} (hδ : IsDiagonalFunction δ) (u v : ↑unitInterval) : BddBelow (Set.range fun (t : ↑unitInterval) => diagUpperAux δ t u v)

theorem ProbabilityTheory.Copula.IsDiagonalFunction.diagUpperInf_le {δ : ↑unitInterval → ℝ} (hδ : IsDiagonalFunction δ) (t u v : ↑unitInterval) : diagUpperInf δ u v ≤ diagUpperAux δ t u v

theorem ProbabilityTheory.Copula.IsDiagonalFunction.diagUpperInf_nonneg {δ : ↑unitInterval → ℝ} (hδ : IsDiagonalFunction δ) (u v : ↑unitInterval) : 0 ≤ diagUpperInf δ u v

theorem ProbabilityTheory.Copula.IsDiagonalFunction.le_diagUpperInf_one {δ : ↑unitInterval → ℝ} (hδ : IsDiagonalFunction δ) (v : ↑unitInterval) : ↑v ≤ diagUpperInf δ 1 v

theorem ProbabilityTheory.Copula.IsQuasiCopula.le_diagUpperAux {Q : (Fin 2 → ↑unitInterval) → ℝ} (hQ : IsQuasiCopula Q) (t u v : ↑unitInterval) : Q ![u, v] ≤ diagUpperAux (fun (s : ↑unitInterval) => Q ![s, s]) t u v

Every bivariate quasi-copula satisfies Q(u,v) ≤ Q(t,t) + (u - t)⁺ + (v - t)⁺ for all t.

theorem ProbabilityTheory.Copula.IsDiagonalFunction.diagUpperInf_eq {δ : ↑unitInterval → ℝ} (hδ : IsDiagonalFunction δ) (u v : ↑unitInterval) : diagUpperInf δ u v = max ↑u ↑v - sSup (diagGap δ '' Set.uIcc u v)

The max-formula of Nelsen, Quesada-Molina, Rodríguez-Lallena and Úbeda-Flores (2004): inf_t (δ t + (u - t)⁺ + (v - t)⁺) = max(u,v) - max_{t ∈ [u ∧ v, u ∨ v]} (t - δ t).

theorem ProbabilityTheory.Copula.diagonalUpperBound_eq {δ : ↑unitInterval → ℝ} (hδ : IsDiagonalFunction δ) (u v : ↑unitInterval) : diagonalUpperBound δ u v = min (min ↑u ↑v) (max ↑u ↑v - sSup (diagGap δ '' Set.uIcc u v))

The upper bound in the form of Nelsen, Quesada-Molina, Rodríguez-Lallena and Úbeda-Flores (2004): A_δ(u,v) = min(u, v, max(u,v) - max_{t ∈ [u ∧ v, u ∨ v]} (t - δ t)).

theorem ProbabilityTheory.Copula.quasiCopula_le_diagonalUpperBound {δ : ↑unitInterval → ℝ} {Q : (Fin 2 → ↑unitInterval) → ℝ} (hQ : IsQuasiCopula Q) (hd : ∀ (t : ↑unitInterval), Q ![t, t] = δ t) (u v : ↑unitInterval) : Q ![u, v] ≤ diagonalUpperBound δ u v

Upper bound for quasi-copulas with a prescribed diagonal (Nelsen, Quesada-Molina, Rodríguez-Lallena and Úbeda-Flores 2004): every bivariate quasi-copula with diagonal δ satisfies Q ≤ A_δ.

theorem ProbabilityTheory.Copula.cdf_le_diagonalUpperBound {δ : ↑unitInterval → ℝ} {C : Copula 2} (hd : ∀ (t : ↑unitInterval), C.diagonal t = δ t) (u v : ↑unitInterval) : C.cdf ![u, v] ≤ diagonalUpperBound δ u v

Upper bound for copulas with a prescribed diagonal: every copula with diagonal δ satisfies C ≤ A_δ.

theorem ProbabilityTheory.Copula.bertino_le_cdf_le_upper {δ : ↑unitInterval → ℝ} (hδ : IsDiagonalFunction δ) {C : Copula 2} (hd : ∀ (t : ↑unitInterval), C.diagonal t = δ t) (u v : ↑unitInterval) : (bertinoCopula δ hδ).cdf ![u, v] ≤ C.cdf ![u, v] ∧ C.cdf ![u, v] ≤ diagonalUpperBound δ u v

Bounds for copulas with a prescribed diagonal: B_δ ≤ C ≤ A_δ for every copula C with diagonal section δ. The lower bound is itself a copula with diagonal δ.

theorem ProbabilityTheory.Copula.diagonalUpperBound_self {δ : ↑unitInterval → ℝ} (hδ : IsDiagonalFunction δ) (t : ↑unitInterval) : diagonalUpperBound δ t t = δ t

The upper bound A_δ has diagonal δ.

theorem ProbabilityTheory.Copula.isQuasiCopula_diagonalUpperBound {δ : ↑unitInterval → ℝ} (hδ : IsDiagonalFunction δ) : IsQuasiCopula fun (u : Fin 2 → ↑unitInterval) => diagonalUpperBound δ (u 0) (u 1)

A_δ is a (bivariate) quasi-copula.

theorem ProbabilityTheory.Copula.diagonalUpperBound_isGreatest {δ : ↑unitInterval → ℝ} (hδ : IsDiagonalFunction δ) : (IsQuasiCopula fun (u : Fin 2 → ↑unitInterval) => diagonalUpperBound δ (u 0) (u 1)) ∧ (∀ (t : ↑unitInterval), diagonalUpperBound δ t t = δ t) ∧ ∀ (Q : (Fin 2 → ↑unitInterval) → ℝ), IsQuasiCopula Q → (∀ (t : ↑unitInterval), Q ![t, t] = δ t) → ∀ (u v : ↑unitInterval), Q ![u, v] ≤ diagonalUpperBound δ u v

A_δ is the largest quasi-copula with diagonal δ: it is a quasi-copula, its diagonal is δ, and it dominates every quasi-copula with diagonal δ.

A sharper bound for copulas, and a diagonal for which A_δ is not attained

theorem ProbabilityTheory.Copula.cdf_le_diagonal_add_diagonal_sub_bertino {δ : ↑unitInterval → ℝ} (hδ : IsDiagonalFunction δ) {C : Copula 2} (hd : ∀ (t : ↑unitInterval), C.diagonal t = δ t) (u v : ↑unitInterval) : C.cdf ![u, v] ≤ δ u + δ v - bertinoKernel δ u v

For copulas the exchange inequality and the Bertino lower bound give C(u,v) ≤ δ(u) + δ(v) - B_δ(u,v).

noncomputable def ProbabilityTheory.Copula.dipGap (t : ↑unitInterval) : ℝ

The gap min(t, 1 - t, 1/10 + |t - 1/2|) of dipDiagonal: two tents joined by a dip.

Equations

• ProbabilityTheory.Copula.dipGap t = min (min (↑t) (1 - ↑t)) (1 / 10 + |↑t - 1 / 2|)

noncomputable def ProbabilityTheory.Copula.dipDiagonal (t : ↑unitInterval) : ℝ

The diagonal δ(t) = t - min(t, 1 - t, 1/10 + |t - 1/2|), i.e. δ = 0 on [0, 3/10], δ(t) = 2t - 3/5 on [3/10, 1/2], δ = 2/5 on [1/2, 7/10] and δ(t) = 2t - 1 on [7/10, 1].

Equations

• ProbabilityTheory.Copula.dipDiagonal t = ↑t - ProbabilityTheory.Copula.dipGap t

theorem ProbabilityTheory.Copula.isDiagonalFunction_dipDiagonal : IsDiagonalFunction dipDiagonal

noncomputable def ProbabilityTheory.Copula.threeTenths : ↑unitInterval

The point 3/10.

Equations

• ProbabilityTheory.Copula.threeTenths = ⟨3 / 10, ProbabilityTheory.Copula.threeTenths._proof_2⟩

noncomputable def ProbabilityTheory.Copula.sevenTenths : ↑unitInterval

The point 7/10.

Equations

• ProbabilityTheory.Copula.sevenTenths = ⟨7 / 10, ProbabilityTheory.Copula.sevenTenths._proof_2⟩

theorem ProbabilityTheory.Copula.diagonalUpperBound_dipDiagonal : diagonalUpperBound dipDiagonal threeTenths sevenTenths = 3 / 10

A_δ(3/10, 7/10) = 3/10 for δ = dipDiagonal.

theorem ProbabilityTheory.Copula.dipDiagonal_gap {C : Copula 2} (hd : ∀ (t : ↑unitInterval), C.diagonal t = dipDiagonal t) : C.cdf ![threeTenths, sevenTenths] ≤ 1 / 5 ∧ C.cdf ![threeTenths, sevenTenths] + 1 / 10 ≤ diagonalUpperBound dipDiagonal threeTenths sevenTenths

A_δ is not best possible for copulas. For δ = dipDiagonal, every copula with diagonal δ satisfies C(3/10, 7/10) ≤ 1/5, whereas A_δ(3/10, 7/10) = 3/10.