Documentation

Copula.Diagonal.Bertino

← Copula mathematical handbook

Bertino copulas: the smallest copula with a prescribed diagonal #

For a diagonal function δ (see IsDiagonalFunction) write δ̂ t = t - δ t for the diagonal gap (diagGap). The Bertino copula of δ is

B_δ(u, v) = min u v - min_{t ∈ [u ∧ v, u ∨ v]} (t - δ t)

(Bertino 1977; Fredricks and Nelsen, The Bertino family of copulas, 2002; see also Nelsen, An Introduction to Copulas, 2nd ed., §3.2.6). The minimum is written as an infimum over the closed interval Set.uIcc u v (bertinoGap).

Main results:

symmetric_twoIncreasing: a symmetric function on [0,1]² is 2-increasing as soon as its rectangle increments are nonnegative on rectangles lying weakly above the diagonal and on squares centred on the diagonal (a general reduction lemma).
bertinoCopula δ hδ: the Bertino copula is a copula, with cdf_bertinoCopula, diagonal_bertinoCopula (its diagonal is δ) and isExchangeable_bertinoCopula.
bertinoCopula_cdf_le, lowerOrthantLE_bertinoCopula: every copula C with diagonal δ satisfies B_δ ≤ C pointwise (Fredricks–Nelsen 2002). Since B_δ itself has diagonal δ, it is the pointwise smallest copula with this diagonal, so the lower bound is best possible.
bertinoCopula_diagonal_comonotonic, bertinoCopula_diagonal_countermonotonic: the Bertino copulas of the diagonals of M and W are M and W.

A reduction lemma for symmetric `2`-increasing functions #

def ProbabilityTheory.Copula.rectIncr (F : ↑unitInterval → ↑unitInterval → ℝ) (a b c e : ↑unitInterval) :

The four-term rectangle increment of a bivariate function on [a,b] × [c,e].

Equations

ProbabilityTheory.Copula.rectIncr F a b c e = F b e - F a e - F b c + F a c

Instances For

theorem ProbabilityTheory.Copula.symmetric_twoIncreasing (F : ↑unitInterval → ↑unitInterval → ℝ) (hF : ∀ (u v : ↑unitInterval), F u v = F v u) (hup : ∀ (a b c e : ↑unitInterval), a ≤ b → b ≤ c → c ≤ e → 0 ≤ F b e - F a e - F b c + F a c) (hsq : ∀ (s t : ↑unitInterval), s ≤ t → 0 ≤ F t t - F s t - F t s + F s s) (a b c e : ↑unitInterval) :

a ≤ b → c ≤ e → 0 ≤ F b e - F a e - F b c + F a c

Reduction lemma for symmetric functions. A symmetric function F on [0,1]² is 2-increasing provided its increments are nonnegative on rectangles [a,b] × [c,e] with b ≤ c (weakly above the diagonal) and on diagonal squares [s,t] × [s,t].

The diagonal gap and its minimum over an interval #

def ProbabilityTheory.Copula.diagGap (δ : ↑unitInterval → ℝ) (t : ↑unitInterval) :

The diagonal gap t - δ t.

Equations

ProbabilityTheory.Copula.diagGap δ t = ↑t - δ t

Instances For

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

The minimum of the diagonal gap over the closed interval between u and v.

Equations

ProbabilityTheory.Copula.bertinoGap δ u v = sInf (ProbabilityTheory.Copula.diagGap δ '' Set.uIcc u v)

Instances For

theorem ProbabilityTheory.Copula.IsDiagonalFunction.zero {δ : ↑unitInterval → ℝ} (hδ : IsDiagonalFunction δ) :

δ 0 = 0

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

0 ≤ diagGap δ t

theorem ProbabilityTheory.Copula.IsDiagonalFunction.diagGap_zero {δ : ↑unitInterval → ℝ} (hδ : IsDiagonalFunction δ) :

diagGap δ 0 = 0

theorem ProbabilityTheory.Copula.IsDiagonalFunction.diagGap_one {δ : ↑unitInterval → ℝ} (hδ : IsDiagonalFunction δ) :

diagGap δ 1 = 0

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

2 * ↑t - 1 ≤ δ t

The lower bound 2t - 1 ≤ δ t.

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

diagGap δ t ≤ 1 - ↑t

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

diagGap δ t ≤ ↑t

theorem ProbabilityTheory.Copula.IsDiagonalFunction.diagGap_sub_le {δ : ↑unitInterval → ℝ} (hδ : IsDiagonalFunction δ) {s t : ↑unitInterval} (hst : s ≤ t) :

diagGap δ t - diagGap δ s ≤ ↑t - ↑s

The diagonal gap does not increase faster than the identity.

theorem ProbabilityTheory.Copula.IsDiagonalFunction.diagGap_sub_ge {δ : ↑unitInterval → ℝ} (hδ : IsDiagonalFunction δ) {s t : ↑unitInterval} (hst : s ≤ t) :

diagGap δ s - diagGap δ t ≤ ↑t - ↑s

The diagonal gap does not decrease faster than the identity.

theorem ProbabilityTheory.Copula.IsDiagonalFunction.continuous {δ : ↑unitInterval → ℝ} (hδ : IsDiagonalFunction δ) :

theorem ProbabilityTheory.Copula.IsDiagonalFunction.continuous_diagGap {δ : ↑unitInterval → ℝ} (hδ : IsDiagonalFunction δ) :

Continuous (diagGap δ)

theorem ProbabilityTheory.Copula.IsDiagonalFunction.bddBelow_diagGap_image {δ : ↑unitInterval → ℝ} (hδ : IsDiagonalFunction δ) (s : Set ↑unitInterval) :

BddBelow (diagGap δ '' s)

theorem ProbabilityTheory.Copula.IsDiagonalFunction.bertinoGap_le {δ : ↑unitInterval → ℝ} (hδ : IsDiagonalFunction δ) {u v t : ↑unitInterval} (ht : t ∈ Set.uIcc u v) :

bertinoGap δ u v ≤ diagGap δ t

theorem ProbabilityTheory.Copula.IsDiagonalFunction.bertinoGap_nonneg {δ : ↑unitInterval → ℝ} (hδ : IsDiagonalFunction δ) (u v : ↑unitInterval) :

0 ≤ bertinoGap δ u v

theorem ProbabilityTheory.Copula.IsDiagonalFunction.bertinoGap_eq_zero {δ : ↑unitInterval → ℝ} (hδ : IsDiagonalFunction δ) {u v t : ↑unitInterval} (ht : t ∈ Set.uIcc u v) (h0 : diagGap δ t = 0) :

bertinoGap δ u v = 0

theorem ProbabilityTheory.Copula.IsDiagonalFunction.bertinoGap_anti {δ : ↑unitInterval → ℝ} (hδ : IsDiagonalFunction δ) {u v u' v' : ↑unitInterval} (h : Set.uIcc u v ⊆ Set.uIcc u' v') :

bertinoGap δ u' v' ≤ bertinoGap δ u v

theorem ProbabilityTheory.Copula.le_bertinoGap {δ : ↑unitInterval → ℝ} {u v : ↑unitInterval} {L : ℝ} (h : ∀ t ∈ Set.uIcc u v, L ≤ diagGap δ t) :

L ≤ bertinoGap δ u v

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

bertinoGap δ u v = bertinoGap δ v u

@[simp]

theorem ProbabilityTheory.Copula.bertinoGap_self {δ : ↑unitInterval → ℝ} (t : ↑unitInterval) :

bertinoGap δ t t = diagGap δ t

The Bertino kernel #

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

The Bertino kernel min u v - min_{t ∈ [u ∧ v, u ∨ v]} (t - δ t).

Equations

ProbabilityTheory.Copula.bertinoKernel δ u v = min ↑u ↑v - ProbabilityTheory.Copula.bertinoGap δ u v

Instances For

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

bertinoKernel δ u v = bertinoKernel δ v u

@[simp]

theorem ProbabilityTheory.Copula.bertinoKernel_self {δ : ↑unitInterval → ℝ} (t : ↑unitInterval) :

bertinoKernel δ t t = δ t

theorem ProbabilityTheory.Copula.bertinoKernel_of_le {δ : ↑unitInterval → ℝ} {u v : ↑unitInterval} (h : u ≤ v) :

bertinoKernel δ u v = ↑u - bertinoGap δ u v

theorem ProbabilityTheory.Copula.IsDiagonalFunction.isClassical_bertino {δ : ↑unitInterval → ℝ} (hδ : IsDiagonalFunction δ) :

IsClassical fun (u : Fin 2 → ↑unitInterval) => bertinoKernel δ (u 0) (u 1)

The Bertino kernel of a diagonal function satisfies the classical copula conditions.

noncomputable def ProbabilityTheory.Copula.bertinoCopula (δ : ↑unitInterval → ℝ) (hδ : IsDiagonalFunction δ) :

The Bertino copula B_δ(u,v) = min u v - min_{t ∈ [u ∧ v, u ∨ v]} (t - δ t) of a diagonal function δ (Fredricks–Nelsen 2002).

Equations

ProbabilityTheory.Copula.bertinoCopula δ hδ = ProbabilityTheory.Copula.ofClassical (fun (u : Fin 2 → ↑unitInterval) => ProbabilityTheory.Copula.bertinoKernel δ (u 0) (u 1)) ⋯

Instances For

theorem ProbabilityTheory.Copula.cdf_bertinoCopula {δ : ↑unitInterval → ℝ} (hδ : IsDiagonalFunction δ) (u : Fin 2 → ↑unitInterval) :

(bertinoCopula δ hδ).cdf u = bertinoKernel δ (u 0) (u 1)

The CDF of the Bertino copula.

@[simp]

theorem ProbabilityTheory.Copula.cdf_bertinoCopula_two {δ : ↑unitInterval → ℝ} (hδ : IsDiagonalFunction δ) (u v : ↑unitInterval) :

(bertinoCopula δ hδ).cdf ![u, v] = bertinoKernel δ u v

@[simp]

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

(bertinoCopula δ hδ).diagonal t = δ t

The Bertino copula of δ has diagonal section δ.

theorem ProbabilityTheory.Copula.isExchangeable_bertinoCopula {δ : ↑unitInterval → ℝ} (hδ : IsDiagonalFunction δ) :

(bertinoCopula δ hδ).IsExchangeable

Bertino copulas are exchangeable.

theorem ProbabilityTheory.Copula.cdf_sub_le_left (C : Copula 2) {s t : ↑unitInterval} (hst : s ≤ t) (v : ↑unitInterval) :

C.cdf ![t, v] - C.cdf ![s, v] ≤ ↑t - ↑s

A bivariate copula CDF increases by at most t - s when its first argument moves from s to t.

theorem ProbabilityTheory.Copula.cdf_sub_le_right (C : Copula 2) {s t : ↑unitInterval} (hst : s ≤ t) (u : ↑unitInterval) :

C.cdf ![u, t] - C.cdf ![u, s] ≤ ↑t - ↑s

A bivariate copula CDF increases by at most t - s when its second argument moves from s to t.

theorem ProbabilityTheory.Copula.cdf_mono_two (C : Copula 2) {u u' v v' : ↑unitInterval} (hu : u ≤ u') (hv : v ≤ v') :

C.cdf ![u, v] ≤ C.cdf ![u', v']

theorem ProbabilityTheory.Copula.bertinoCopula_cdf_le {δ : ↑unitInterval → ℝ} (hδ : IsDiagonalFunction δ) {C : Copula 2} (hC : ∀ (t : ↑unitInterval), C.diagonal t = δ t) (u v : ↑unitInterval) :

(bertinoCopula δ hδ).cdf ![u, v] ≤ C.cdf ![u, v]

The Bertino copula is the smallest copula with diagonal δ (Fredricks–Nelsen 2002): every copula C with diagonal section δ satisfies B_δ ≤ C pointwise.

theorem ProbabilityTheory.Copula.lowerOrthantLE_bertinoCopula {δ : ↑unitInterval → ℝ} (hδ : IsDiagonalFunction δ) {C : Copula 2} (hC : ∀ (t : ↑unitInterval), C.diagonal t = δ t) :

(bertinoCopula δ hδ).LowerOrthantLE C

The Bertino copula of δ lies below every copula with diagonal δ in the lower orthant order.

theorem ProbabilityTheory.Copula.lowerOrthantLE_bertinoCopula_diagonal (C : Copula 2) :

(bertinoCopula C.diagonal ⋯).LowerOrthantLE C

The Bertino copula of the diagonal of a copula lies below that copula.

theorem ProbabilityTheory.Copula.bertinoCopula_diagonal_comonotonic :

bertinoCopula (comonotonic 2).diagonal ⋯ = comonotonic 2

The Bertino copula of the diagonal of M is M.

theorem ProbabilityTheory.Copula.bertinoCopula_diagonal_countermonotonic :

bertinoCopula countermonotonic.diagonal ⋯ = countermonotonic

The Bertino copula of the diagonal of W is W: the countermonotonic copula is the smallest copula with its diagonal.