Quadrant, tail and stochastic positive dependence #

LTD, RTI and SI refer to coordinate 1 given coordinate 0. The division-free tail inequalities include the boundary points. SI uses the equivalent CDF concavity characterization, written with chord lengths.

source

@[simp]

theorem ProbabilityTheory.Copula.cdf_two_zero_left (C : Copula 2) (v : ↑unitInterval) :

C.cdf ![0, v] = 0

source

@[simp]

theorem ProbabilityTheory.Copula.cdf_two_one_left (C : Copula 2) (v : ↑unitInterval) :

C.cdf ![1, v] = ↑v

source

@[simp]

theorem ProbabilityTheory.Copula.cdf_two_one_right (C : Copula 2) (u : ↑unitInterval) :

C.cdf ![u, 1] = ↑u

source

def ProbabilityTheory.Copula.IsPQD (C : Copula 2) :

Prop

Positive quadrant dependence.

Equations

C.IsPQD = ∀ (u v : ↑unitInterval), ↑u * ↑v ≤ C.cdf ![u, v]

Instances For

source

def ProbabilityTheory.Copula.IsNQD (C : Copula 2) :

Prop

Negative quadrant dependence.

Equations

C.IsNQD = ∀ (u v : ↑unitInterval), C.cdf ![u, v] ≤ ↑u * ↑v

Instances For

source

def ProbabilityTheory.Copula.IsLTD (C : Copula 2) :

Prop

Left-tail decreasing: P(V ≤ v | U ≤ u) decreases in u > 0.

Equations

C.IsLTD = ∀ (a b v : ↑unitInterval), a ≤ b → ↑a * C.cdf ![b, v] ≤ ↑b * C.cdf ![a, v]

Instances For

source

def ProbabilityTheory.Copula.IsRTI (C : Copula 2) :

Prop

Right-tail increasing: P(V > v | U > u) increases in u < 1. Equivalently, the upper-tail conditional CDF decreases.

Equations

C.IsRTI = ∀ (a b v : ↑unitInterval), a ≤ b → (1 - ↑a) * (↑v - C.cdf ![b, v]) ≤ (1 - ↑b) * (↑v - C.cdf ![a, v])

Instances For

source

def ProbabilityTheory.Copula.IsSI (C : Copula 2) :

Prop

Stochastic increasingness via concavity of every first-coordinate CDF section. The chord inequality avoids division by zero, including coincident endpoints.

Equations

C.IsSI = ∀ (a b c v : ↑unitInterval), a ≤ b → b ≤ c → (↑b - ↑a) * C.cdf ![c, v] + (↑c - ↑b) * C.cdf ![a, v] ≤ (↑c - ↑a) * C.cdf ![b, v]

Instances For

source

theorem ProbabilityTheory.Copula.IsLTD.isPQD {C : Copula 2} (h : C.IsLTD) :

C.IsPQD

source

theorem ProbabilityTheory.Copula.IsRTI.isPQD {C : Copula 2} (h : C.IsRTI) :

C.IsPQD

source

theorem ProbabilityTheory.Copula.IsSI.isLTD {C : Copula 2} (h : C.IsSI) :

C.IsLTD

source

theorem ProbabilityTheory.Copula.IsSI.isRTI {C : Copula 2} (h : C.IsSI) :

C.IsRTI

source

theorem ProbabilityTheory.Copula.IsSI.isPQD {C : Copula 2} (h : C.IsSI) :

C.IsPQD

source

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

C.IsLTD ↔ ∀ (v : ↑unitInterval), AntitoneOn (fun (u : ↑unitInterval) => C.cdf ![u, v] / ↑u) (Set.Ioi 0)

source

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

C.IsRTI ↔ ∀ (v : ↑unitInterval), AntitoneOn (fun (u : ↑unitInterval) => (↑v - C.cdf ![u, v]) / (1 - ↑u)) (Set.Iio 1)

source

theorem ProbabilityTheory.Copula.IsPQD.mix {C D : Copula 2} (hC : C.IsPQD) (hD : D.IsPQD) (w : ↑unitInterval) :

(C.mix D w).IsPQD

source

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

C.IsRTI ↔ ∀ (v : ↑unitInterval), MonotoneOn (fun (u : ↑unitInterval) => (1 - ↑u - ↑v + C.cdf ![u, v]) / (1 - ↑u)) (Set.Iio 1)

The usual survival-probability formulation of RTI.

source

theorem ProbabilityTheory.Copula.IsLTD.mix {C D : Copula 2} (hC : C.IsLTD) (hD : D.IsLTD) (w : ↑unitInterval) :

(C.mix D w).IsLTD

source

theorem ProbabilityTheory.Copula.IsRTI.mix {C D : Copula 2} (hC : C.IsRTI) (hD : D.IsRTI) (w : ↑unitInterval) :

(C.mix D w).IsRTI

source

theorem ProbabilityTheory.Copula.IsSI.mix {C D : Copula 2} (hC : C.IsSI) (hD : D.IsSI) (w : ↑unitInterval) :

(C.mix D w).IsSI

Documentation

Copula.Dependence.Basic

Quadrant, tail and stochastic positive dependence #