Documentation

Copula.Dependence.HierarchyExamples

← Copula mathematical handbook

Strictness of the positive dependence hierarchy #

Product perturbations C(u,v) = uv + φ(u) ψ(v) of independence (Copula.Families.ProductPerturbation) with piecewise linear profiles separate the levels of the positive dependence hierarchy of Nelsen, An Introduction to Copulas, 2nd ed., §5.2. Writing D = C - Π = φ ⊗ ψ with ψ ≥ 0:

LTD holds iff φ(u)/u is nonincreasing, RTI iff φ(u)/(1-u) is nondecreasing, SI iff φ is concave, and PQD iff φ ≥ 0 (sufficient directions proved here);
the tent τ(t) = min(t, 1-t), the bumps max(0, min(t - 1/2, 1 - t)) and max(0, min(t, 1/2 - t)) and the two-peak profile max(min(t, (1-t)/3), min(t/3, 1-t)) give:

copula	PQD	LTD	RTI	SI	SI of transpose
`rightBumpCopula`	yes	no	yes	no
`leftBumpCopula`	yes	yes	no	no
`twoPeakCopula`	yes	yes	yes	no
`tentTwoPeakCopula`	yes	yes	yes	yes	no

Hence PQD ⇏ LTD, PQD ⇏ RTI, RTI ⇏ LTD, LTD ⇏ RTI, LTD ∧ RTI ⇏ SI (the hypothesis of the Capéraà–Genest inequality is strictly weaker than SI), and SI(V|U) ⇏ SI(U|V).

Profile conditions #

def ProbabilityTheory.Copula.HierarchyExamples.LTDProfile (f : ↑unitInterval → ℝ) :

Profile condition for LTD: φ(u)/u is nonincreasing (cross-multiplied).

Equations

ProbabilityTheory.Copula.HierarchyExamples.LTDProfile f = ∀ (a b : ↑unitInterval), a ≤ b → ↑a * f b ≤ ↑b * f a

Instances For

def ProbabilityTheory.Copula.HierarchyExamples.RTIProfile (f : ↑unitInterval → ℝ) :

Profile condition for RTI: φ(u)/(1-u) is nondecreasing (cross-multiplied).

Equations

ProbabilityTheory.Copula.HierarchyExamples.RTIProfile f = ∀ (a b : ↑unitInterval), a ≤ b → (1 - ↑b) * f a ≤ (1 - ↑a) * f b

Instances For

def ProbabilityTheory.Copula.HierarchyExamples.ChordConcave (f : ↑unitInterval → ℝ) :

Profile condition for SI: concavity in chord form.

Equations

ProbabilityTheory.Copula.HierarchyExamples.ChordConcave f = ∀ (a b c : ↑unitInterval), a ≤ b → b ≤ c → (↑b - ↑a) * f c + (↑c - ↑b) * f a ≤ (↑c - ↑a) * f b

Instances For

theorem ProbabilityTheory.Copula.HierarchyExamples.LTDProfile.min {f g : ↑unitInterval → ℝ} (hf : LTDProfile f) (hg : LTDProfile g) :

LTDProfile fun (t : ↑unitInterval) => Min.min (f t) (g t)

theorem ProbabilityTheory.Copula.HierarchyExamples.LTDProfile.max {f g : ↑unitInterval → ℝ} (hf : LTDProfile f) (hg : LTDProfile g) :

LTDProfile fun (t : ↑unitInterval) => Max.max (f t) (g t)

theorem ProbabilityTheory.Copula.HierarchyExamples.ltdProfile_affine {f : ↑unitInterval → ℝ} (m k : ℝ) (hk : 0 ≤ k) (hf : ∀ (t : ↑unitInterval), f t = m * ↑t + k) :

theorem ProbabilityTheory.Copula.HierarchyExamples.RTIProfile.min {f g : ↑unitInterval → ℝ} (hf : RTIProfile f) (hg : RTIProfile g) :

RTIProfile fun (t : ↑unitInterval) => Min.min (f t) (g t)

theorem ProbabilityTheory.Copula.HierarchyExamples.RTIProfile.max {f g : ↑unitInterval → ℝ} (hf : RTIProfile f) (hg : RTIProfile g) :

RTIProfile fun (t : ↑unitInterval) => Max.max (f t) (g t)

theorem ProbabilityTheory.Copula.HierarchyExamples.rtiProfile_affine {f : ↑unitInterval → ℝ} (m k : ℝ) (hk : 0 ≤ m + k) (hf : ∀ (t : ↑unitInterval), f t = m * ↑t + k) :

theorem ProbabilityTheory.Copula.HierarchyExamples.ChordConcave.min {f g : ↑unitInterval → ℝ} (hf : ChordConcave f) (hg : ChordConcave g) :

ChordConcave fun (t : ↑unitInterval) => Min.min (f t) (g t)

theorem ProbabilityTheory.Copula.HierarchyExamples.chordConcave_affine {f : ↑unitInterval → ℝ} (m k : ℝ) (hf : ∀ (t : ↑unitInterval), f t = m * ↑t + k) :

Dependence properties of product perturbations #

theorem ProbabilityTheory.Copula.HierarchyExamples.productPerturbation_isPQD {φ ψ : BoundaryProfile} {h : φ.lip * ψ.lip ≤ 1} (hφ : ∀ (t : ↑unitInterval), 0 ≤ φ.toFun t) (hψ : ∀ (t : ↑unitInterval), 0 ≤ ψ.toFun t) :

(productPerturbation φ ψ h).IsPQD

theorem ProbabilityTheory.Copula.HierarchyExamples.productPerturbation_isLTD {φ ψ : BoundaryProfile} {h : φ.lip * ψ.lip ≤ 1} (hψ : ∀ (t : ↑unitInterval), 0 ≤ ψ.toFun t) (hφ : LTDProfile φ.toFun) :

(productPerturbation φ ψ h).IsLTD

theorem ProbabilityTheory.Copula.HierarchyExamples.productPerturbation_isRTI {φ ψ : BoundaryProfile} {h : φ.lip * ψ.lip ≤ 1} (hψ : ∀ (t : ↑unitInterval), 0 ≤ ψ.toFun t) (hφ : RTIProfile φ.toFun) :

(productPerturbation φ ψ h).IsRTI

theorem ProbabilityTheory.Copula.HierarchyExamples.productPerturbation_isSI {φ ψ : BoundaryProfile} {h : φ.lip * ψ.lip ≤ 1} (hψ : ∀ (t : ↑unitInterval), 0 ≤ ψ.toFun t) (hφ : ChordConcave φ.toFun) :

(productPerturbation φ ψ h).IsSI

theorem ProbabilityTheory.Copula.HierarchyExamples.productPerturbation_transpose {φ ψ : BoundaryProfile} {h : φ.lip * ψ.lip ≤ 1} (h' : ψ.lip * φ.lip ≤ 1) :

(productPerturbation φ ψ h).transpose = productPerturbation ψ φ h'

The transpose of Π + φ ⊗ ψ is Π + ψ ⊗ φ.

Piecewise linear profiles #

noncomputable def ProbabilityTheory.Copula.HierarchyExamples.tent :

BoundaryProfile

The tent profile min(t, 1 - t).

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def ProbabilityTheory.Copula.HierarchyExamples.rightBump :

BoundaryProfile

A bump supported on [1/2, 1]: max(0, min(t - 1/2, 1 - t)).

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def ProbabilityTheory.Copula.HierarchyExamples.leftBump :

BoundaryProfile

A bump supported on [0, 1/2]: max(0, min(t, 1/2 - t)).

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def ProbabilityTheory.Copula.HierarchyExamples.twoPeak :

BoundaryProfile

A non-concave profile with two peaks: max(min(t, (1-t)/3), min(t/3, 1-t)).

Equations

One or more equations did not get rendered due to their size.

Instances For

@[simp]

theorem ProbabilityTheory.Copula.HierarchyExamples.tent_apply (t : ↑unitInterval) :

tent.toFun t = min (↑t) (1 - ↑t)

@[simp]

theorem ProbabilityTheory.Copula.HierarchyExamples.rightBump_apply (t : ↑unitInterval) :

rightBump.toFun t = max 0 (min (↑t - 1 / 2) (1 - ↑t))

@[simp]

theorem ProbabilityTheory.Copula.HierarchyExamples.leftBump_apply (t : ↑unitInterval) :

leftBump.toFun t = max 0 (min (↑t) (1 / 2 - ↑t))

@[simp]

theorem ProbabilityTheory.Copula.HierarchyExamples.twoPeak_apply (t : ↑unitInterval) :

twoPeak.toFun t = max (min (↑t) ((1 - ↑t) / 3)) (min (↑t / 3) (1 - ↑t))

theorem ProbabilityTheory.Copula.HierarchyExamples.tent_nonneg (t : ↑unitInterval) :

0 ≤ tent.toFun t

theorem ProbabilityTheory.Copula.HierarchyExamples.rightBump_nonneg (t : ↑unitInterval) :

0 ≤ rightBump.toFun t

theorem ProbabilityTheory.Copula.HierarchyExamples.leftBump_nonneg (t : ↑unitInterval) :

0 ≤ leftBump.toFun t

theorem ProbabilityTheory.Copula.HierarchyExamples.twoPeak_nonneg (t : ↑unitInterval) :

0 ≤ twoPeak.toFun t

theorem ProbabilityTheory.Copula.HierarchyExamples.tent_ltd :

LTDProfile tent.toFun

theorem ProbabilityTheory.Copula.HierarchyExamples.tent_rti :

RTIProfile tent.toFun

theorem ProbabilityTheory.Copula.HierarchyExamples.tent_concave :

ChordConcave tent.toFun

theorem ProbabilityTheory.Copula.HierarchyExamples.rightBump_rti :

RTIProfile rightBump.toFun

theorem ProbabilityTheory.Copula.HierarchyExamples.leftBump_ltd :

LTDProfile leftBump.toFun

theorem ProbabilityTheory.Copula.HierarchyExamples.twoPeak_ltd :

LTDProfile twoPeak.toFun

theorem ProbabilityTheory.Copula.HierarchyExamples.twoPeak_rti :

RTIProfile twoPeak.toFun

The four copulas #

noncomputable def ProbabilityTheory.Copula.HierarchyExamples.rightBumpCopula :

Π + rightBump ⊗ tent: RTI and PQD but not LTD.

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def ProbabilityTheory.Copula.HierarchyExamples.leftBumpCopula :

Π + leftBump ⊗ tent: LTD and PQD but not RTI.

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def ProbabilityTheory.Copula.HierarchyExamples.twoPeakCopula :

Π + twoPeak ⊗ tent: LTD and RTI but not SI.

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def ProbabilityTheory.Copula.HierarchyExamples.tentTwoPeakCopula :

Π + tent ⊗ twoPeak: SI, but its transpose is not SI.

Equations

One or more equations did not get rendered due to their size.

Instances For

theorem ProbabilityTheory.Copula.HierarchyExamples.isRTI_rightBumpCopula :

rightBumpCopula.IsRTI

theorem ProbabilityTheory.Copula.HierarchyExamples.isPQD_rightBumpCopula :

rightBumpCopula.IsPQD

theorem ProbabilityTheory.Copula.HierarchyExamples.not_isLTD_rightBumpCopula :

¬rightBumpCopula.IsLTD

theorem ProbabilityTheory.Copula.HierarchyExamples.not_isSI_rightBumpCopula :

¬rightBumpCopula.IsSI

theorem ProbabilityTheory.Copula.HierarchyExamples.isLTD_leftBumpCopula :

leftBumpCopula.IsLTD

theorem ProbabilityTheory.Copula.HierarchyExamples.isPQD_leftBumpCopula :

leftBumpCopula.IsPQD

theorem ProbabilityTheory.Copula.HierarchyExamples.not_isRTI_leftBumpCopula :

¬leftBumpCopula.IsRTI

theorem ProbabilityTheory.Copula.HierarchyExamples.not_isSI_leftBumpCopula :

¬leftBumpCopula.IsSI

theorem ProbabilityTheory.Copula.HierarchyExamples.isLTD_twoPeakCopula :

twoPeakCopula.IsLTD

theorem ProbabilityTheory.Copula.HierarchyExamples.isRTI_twoPeakCopula :

twoPeakCopula.IsRTI

theorem ProbabilityTheory.Copula.HierarchyExamples.not_isSI_twoPeakCopula :

¬twoPeakCopula.IsSI

LTD and RTI together do not imply SI.

theorem ProbabilityTheory.Copula.HierarchyExamples.isSI_tentTwoPeakCopula :

tentTwoPeakCopula.IsSI

theorem ProbabilityTheory.Copula.HierarchyExamples.transpose_tentTwoPeakCopula :

tentTwoPeakCopula.transpose = twoPeakCopula

theorem ProbabilityTheory.Copula.HierarchyExamples.not_isSI_transpose_tentTwoPeakCopula :

¬tentTwoPeakCopula.transpose.IsSI

Stochastic increasingness of V in U does not imply that of U in V.

theorem ProbabilityTheory.Copula.HierarchyExamples.not_isCI_tentTwoPeakCopula :

¬tentTwoPeakCopula.IsCI