← Mathematical handbook

Section 2 of the article (version 2): classes, reflection and interpolation

• (2.2): 1 - ξ(C) = 6 ∫∫ h (1 - h) with h = ∂₁C.
• (2.3): ξ(Č) = ξ(C), β(Č) = -β(C) for Č(u,v) = u - C(u, 1-v) (the library's C.reflect {1}).
• the five classes PQD, NQD, SI, SD, RS, their convexity, the involution C ↦ Č and the reflection (2.4) of the (ξ, β)-regions of the classes and their intersections.
• Lemma 2.1 (interpolation in a convex subclass).

Equation (2.2)

theorem Papers.OrendayLaresRockel2026XiBeta.one_sub_xi_eq (C : ProbabilityTheory.Copula 2) : 1 - C.chatterjeeXi = 6 * ∫ (v : ↑unitInterval) (u : ↑unitInterval), C.conditionalCDF u v * (1 - C.conditionalCDF u v)

Equation (2.2), with the Markov kernel h(u,v) = ∂₁C(u,v) = K_C(u,[0,v]).

theorem Papers.OrendayLaresRockel2026XiBeta.one_sub_xi_eq_deriv (C : ProbabilityTheory.Copula 2) : 1 - C.chatterjeeXi = 6 * ∫ (v : ↑unitInterval) (u : ↑unitInterval), deriv (C.cdfSection v) ↑u * (1 - deriv (C.cdfSection v) ↑u)

Equation (2.2) with the classical partial derivative ∂₁C(u,v) (equal to the kernel for Lebesgue-a.e. u).

Equation (2.3): the involution C ↦ Č

theorem Papers.OrendayLaresRockel2026XiBeta.check_cdf (C : ProbabilityTheory.Copula 2) (u v : ↑unitInterval) : (C.reflect {1}).cdf ![u, v] = ↑u - C.cdf ![u, unitInterval.symm v]

Č(u,v) = u - C(u, 1 - v).

theorem Papers.OrendayLaresRockel2026XiBeta.xi_check (C : ProbabilityTheory.Copula 2) : (C.reflect {1}).chatterjeeXi = C.chatterjeeXi

Equation (2.3), first part.

theorem Papers.OrendayLaresRockel2026XiBeta.beta_check (C : ProbabilityTheory.Copula 2) : (C.reflect {1}).blomqvistBeta = -C.blomqvistBeta

Equation (2.3), second part.

theorem Papers.OrendayLaresRockel2026XiBeta.check_kernel (C : ProbabilityTheory.Copula 2) (v : ↑unitInterval) : (fun (u : ↑unitInterval) => (C.reflect {1}).conditionalCDF u v) =ᵐ[MeasureTheory.volume] fun (u : ↑unitInterval) => 1 - C.conditionalCDF u (unitInterval.symm v)

The kernel of Č: ∂₁Č(u,v) = 1 - ∂₁C(u, 1 - v) for a.e. u.

The five classes, convexity and the involution

def Papers.OrendayLaresRockel2026XiBeta.classPQD : Set (ProbabilityTheory.Copula 2)

Positive quadrant dependent copulas.

Equations

• Papers.OrendayLaresRockel2026XiBeta.classPQD = {C : ProbabilityTheory.Copula 2 | C.IsPQD}

def Papers.OrendayLaresRockel2026XiBeta.classNQD : Set (ProbabilityTheory.Copula 2)

Negative quadrant dependent copulas.

Equations

• Papers.OrendayLaresRockel2026XiBeta.classNQD = {C : ProbabilityTheory.Copula 2 | C.IsNQD}

def Papers.OrendayLaresRockel2026XiBeta.classSI : Set (ProbabilityTheory.Copula 2)

Stochastically increasing copulas.

Equations

• Papers.OrendayLaresRockel2026XiBeta.classSI = {C : ProbabilityTheory.Copula 2 | C.IsSI}

def Papers.OrendayLaresRockel2026XiBeta.classSD : Set (ProbabilityTheory.Copula 2)

Stochastically decreasing copulas.

Equations

• Papers.OrendayLaresRockel2026XiBeta.classSD = {C : ProbabilityTheory.Copula 2 | C.IsSD}

def Papers.OrendayLaresRockel2026XiBeta.classRS : Set (ProbabilityTheory.Copula 2)

Radially symmetric copulas.

Equations

• Papers.OrendayLaresRockel2026XiBeta.classRS = {C : ProbabilityTheory.Copula 2 | C.IsRadiallySymmetric}

def Papers.OrendayLaresRockel2026XiBeta.IsConvexClass (A : Set (ProbabilityTheory.Copula 2)) : Prop

A class of copulas is convex if it is closed under mixtures.

Equations

• Papers.OrendayLaresRockel2026XiBeta.IsConvexClass A = ∀ C ∈ A, ∀ D ∈ A, ∀ (a : ↑unitInterval), C.mix D a ∈ A

theorem Papers.OrendayLaresRockel2026XiBeta.isNQD_mix {C D : ProbabilityTheory.Copula 2} (hC : C.IsNQD) (hD : D.IsNQD) (w : ↑unitInterval) : (C.mix D w).IsNQD

theorem Papers.OrendayLaresRockel2026XiBeta.isSD_mix {C D : ProbabilityTheory.Copula 2} (hC : C.IsSD) (hD : D.IsSD) (w : ↑unitInterval) : (C.mix D w).IsSD

theorem Papers.OrendayLaresRockel2026XiBeta.convex_univ : IsConvexClass Set.univ

theorem Papers.OrendayLaresRockel2026XiBeta.convex_pqd : IsConvexClass classPQD

theorem Papers.OrendayLaresRockel2026XiBeta.convex_nqd : IsConvexClass classNQD

theorem Papers.OrendayLaresRockel2026XiBeta.convex_si : IsConvexClass classSI

theorem Papers.OrendayLaresRockel2026XiBeta.convex_sd : IsConvexClass classSD

theorem Papers.OrendayLaresRockel2026XiBeta.convex_rs : IsConvexClass classRS

theorem Papers.OrendayLaresRockel2026XiBeta.IsConvexClass.inter {A B : Set (ProbabilityTheory.Copula 2)} (hA : IsConvexClass A) (hB : IsConvexClass B) : IsConvexClass (A ∩ B)

Intersections of convex classes are convex (so all intersections of the five classes are).

theorem Papers.OrendayLaresRockel2026XiBeta.classSI_subset_classPQD : classSI ⊆ classPQD

Every SI copula is PQD.

theorem Papers.OrendayLaresRockel2026XiBeta.classSD_subset_classNQD : classSD ⊆ classNQD

Every SD copula is NQD.

theorem Papers.OrendayLaresRockel2026XiBeta.isPQD_reflect_second_iff (C : ProbabilityTheory.Copula 2) : (C.reflect {1}).IsPQD ↔ C.IsNQD

theorem Papers.OrendayLaresRockel2026XiBeta.isNQD_reflect_second_iff (C : ProbabilityTheory.Copula 2) : (C.reflect {1}).IsNQD ↔ C.IsPQD

theorem Papers.OrendayLaresRockel2026XiBeta.isRadiallySymmetric_reflect_second_iff (C : ProbabilityTheory.Copula 2) : (C.reflect {1}).IsRadiallySymmetric ↔ C.IsRadiallySymmetric

def Papers.OrendayLaresRockel2026XiBeta.checkClass (A : Set (ProbabilityTheory.Copula 2)) : Set (ProbabilityTheory.Copula 2)

Ǎ = {Č : C ∈ A}.

Equations

• Papers.OrendayLaresRockel2026XiBeta.checkClass A = (fun (C : ProbabilityTheory.Copula 2) => C.reflect {1}) '' A

theorem Papers.OrendayLaresRockel2026XiBeta.mem_checkClass_iff (A : Set (ProbabilityTheory.Copula 2)) (D : ProbabilityTheory.Copula 2) : D ∈ checkClass A ↔ D.reflect {1} ∈ A

theorem Papers.OrendayLaresRockel2026XiBeta.checkClass_pqd : checkClass classPQD = classNQD

theorem Papers.OrendayLaresRockel2026XiBeta.checkClass_nqd : checkClass classNQD = classPQD

theorem Papers.OrendayLaresRockel2026XiBeta.checkClass_si : checkClass classSI = classSD

theorem Papers.OrendayLaresRockel2026XiBeta.checkClass_sd : checkClass classSD = classSI

theorem Papers.OrendayLaresRockel2026XiBeta.checkClass_rs : checkClass classRS = classRS

theorem Papers.OrendayLaresRockel2026XiBeta.checkClass_univ : checkClass Set.univ = Set.univ

theorem Papers.OrendayLaresRockel2026XiBeta.checkClass_inter (A B : Set (ProbabilityTheory.Copula 2)) : checkClass (A ∩ B) = checkClass A ∩ checkClass B

Equation (2.4)

def Papers.OrendayLaresRockel2026XiBeta.xiBetaRegion (A : Set (ProbabilityTheory.Copula 2)) : Set (ℝ × ℝ)

R^A_{ξ,β} = {(ξ(C), β(C)) : C ∈ A}.

Equations

• Papers.OrendayLaresRockel2026XiBeta.xiBetaRegion A = {p : ℝ × ℝ | ∃ C ∈ A, C.chatterjeeXi = p.1 ∧ C.blomqvistBeta = p.2}

theorem Papers.OrendayLaresRockel2026XiBeta.xiBetaRegion_checkClass (A : Set (ProbabilityTheory.Copula 2)) : xiBetaRegion (checkClass A) = (fun (p : ℝ × ℝ) => (p.1, -p.2)) '' xiBetaRegion A

Equation (2.4): R^{Ǎ} = {(x, -y) : (x, y) ∈ R^A} for every class A.

theorem Papers.OrendayLaresRockel2026XiBeta.xiBetaRegion_nqd_eq : xiBetaRegion classNQD = (fun (p : ℝ × ℝ) => (p.1, -p.2)) '' xiBetaRegion classPQD

Equation (2.4) for the five classes: the mirror image of PQD is NQD, etc.

theorem Papers.OrendayLaresRockel2026XiBeta.xiBetaRegion_sd_eq : xiBetaRegion classSD = (fun (p : ℝ × ℝ) => (p.1, -p.2)) '' xiBetaRegion classSI

theorem Papers.OrendayLaresRockel2026XiBeta.xiBetaRegion_rs_eq : xiBetaRegion classRS = (fun (p : ℝ × ℝ) => (p.1, -p.2)) '' xiBetaRegion classRS

theorem Papers.OrendayLaresRockel2026XiBeta.xiBetaRegion_mono {A B : Set (ProbabilityTheory.Copula 2)} (h : A ⊆ B) : xiBetaRegion A ⊆ xiBetaRegion B

Lemma 2.1 (interpolation)

theorem Papers.OrendayLaresRockel2026XiBeta.interpolation_lemma {A : Set (ProbabilityTheory.Copula 2)} (hA : IsConvexClass A) {C₀ C₁ : ProbabilityTheory.Copula 2} (h₀ : C₀ ∈ A) (h₁ : C₁ ∈ A) {b : ℝ} (hb₀ : C₀.blomqvistBeta = b) (hb₁ : C₁.blomqvistBeta = b) {x : ℝ} (hx : x ∈ Set.uIcc C₀.chatterjeeXi C₁.chatterjeeXi) : ∃ C ∈ A, C.chatterjeeXi = x ∧ C.blomqvistBeta = b

Lemma 2.1. Let A be convex and C₀, C₁ ∈ A with β(C₀) = β(C₁) = b. For every x between ξ(C₀) and ξ(C₁) there is C ∈ A with ξ(C) = x and β(C) = b.

Stochastic monotonicity via kernel versions

theorem Papers.OrendayLaresRockel2026XiBeta.isSI_iff_antitone_version (C : ProbabilityTheory.Copula 2) : C.IsSI ↔ ∀ (v : ↑unitInterval), ∃ (g : ↑unitInterval → ℝ), Antitone g ∧ (fun (u : ↑unitInterval) => C.conditionalCDF u v) =ᵐ[MeasureTheory.volume] g

SI means that for every v the kernel u ↦ ∂₁C(u,v) has a nonincreasing version (equivalently, C(·, v) is concave).

theorem Papers.OrendayLaresRockel2026XiBeta.isSD_iff_monotone_version (C : ProbabilityTheory.Copula 2) : C.IsSD ↔ ∀ (v : ↑unitInterval), ∃ (g : ↑unitInterval → ℝ), Monotone g ∧ (fun (u : ↑unitInterval) => C.conditionalCDF u v) =ᵐ[MeasureTheory.volume] g

SD means that for every v the kernel has a nondecreasing version.

theorem Papers.OrendayLaresRockel2026XiBeta.transpose_isSI_iff_concave (C : ProbabilityTheory.Copula 2) : C.transpose.IsSI ↔ ∀ (a b c u : ↑unitInterval), a ≤ b → b ≤ c → (↑b - ↑a) * C.cdf ![u, c] + (↑c - ↑b) * C.cdf ![u, a] ≤ (↑c - ↑a) * C.cdf ![u, b]

C^⊤ is SI iff v ↦ C(u,v) is concave for every u.

All intersections of the five classes

inductive Papers.OrendayLaresRockel2026XiBeta.Cls : Type

The five classes of the article.

• pqd : Cls
• nqd : Cls
• si : Cls
• sd : Cls
• rs : Cls

@[instance_reducible]

instance Papers.OrendayLaresRockel2026XiBeta.instDecidableEqCls : DecidableEq Cls

Equations

• Papers.OrendayLaresRockel2026XiBeta.instDecidableEqCls x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Papers.OrendayLaresRockel2026XiBeta.Cls.set : Cls → Set (ProbabilityTheory.Copula 2)

The class of copulas denoted by a symbol.

Equations

• Papers.OrendayLaresRockel2026XiBeta.Cls.pqd.set = Papers.OrendayLaresRockel2026XiBeta.classPQD
• Papers.OrendayLaresRockel2026XiBeta.Cls.nqd.set = Papers.OrendayLaresRockel2026XiBeta.classNQD
• Papers.OrendayLaresRockel2026XiBeta.Cls.si.set = Papers.OrendayLaresRockel2026XiBeta.classSI
• Papers.OrendayLaresRockel2026XiBeta.Cls.sd.set = Papers.OrendayLaresRockel2026XiBeta.classSD
• Papers.OrendayLaresRockel2026XiBeta.Cls.rs.set = Papers.OrendayLaresRockel2026XiBeta.classRS

def Papers.OrendayLaresRockel2026XiBeta.Cls.check : Cls → Cls

The image of a class under C ↦ Č.

Equations

• Papers.OrendayLaresRockel2026XiBeta.Cls.pqd.check = Papers.OrendayLaresRockel2026XiBeta.Cls.nqd
• Papers.OrendayLaresRockel2026XiBeta.Cls.nqd.check = Papers.OrendayLaresRockel2026XiBeta.Cls.pqd
• Papers.OrendayLaresRockel2026XiBeta.Cls.si.check = Papers.OrendayLaresRockel2026XiBeta.Cls.sd
• Papers.OrendayLaresRockel2026XiBeta.Cls.sd.check = Papers.OrendayLaresRockel2026XiBeta.Cls.si
• Papers.OrendayLaresRockel2026XiBeta.Cls.rs.check = Papers.OrendayLaresRockel2026XiBeta.Cls.rs

def Papers.OrendayLaresRockel2026XiBeta.interSet (S : Finset Cls) : Set (ProbabilityTheory.Copula 2)

The intersection of the classes in S (the whole class of copulas for S = ∅).

Equations

• Papers.OrendayLaresRockel2026XiBeta.interSet S = {C : ProbabilityTheory.Copula 2 | ∀ c ∈ S, C ∈ c.set}

theorem Papers.OrendayLaresRockel2026XiBeta.checkClass_cls (c : Cls) : checkClass c.set = c.check.set

theorem Papers.OrendayLaresRockel2026XiBeta.convex_cls (c : Cls) : IsConvexClass c.set

theorem Papers.OrendayLaresRockel2026XiBeta.convex_interSet (S : Finset Cls) : IsConvexClass (interSet S)

Every intersection of the five classes is convex.

theorem Papers.OrendayLaresRockel2026XiBeta.checkClass_interSet (S : Finset Cls) : checkClass (interSet S) = interSet (Finset.image Cls.check S)

Ǎ for an intersection A of the five classes is the intersection of the mirrored classes.

theorem Papers.OrendayLaresRockel2026XiBeta.xiBetaRegion_interSet_check (S : Finset Cls) : xiBetaRegion (interSet (Finset.image Cls.check S)) = (fun (p : ℝ × ℝ) => (p.1, -p.2)) '' xiBetaRegion (interSet S)

Equation (2.4) for each of the five classes and each intersection of them: R^{Ǎ} = {(x, -y) : (x, y) ∈ R^A}.