Extreme-value CDF order and explicit monotone families #

source

theorem Papers.AnsariRockel2024.extremeValue_pickands_order (C D : ProbabilityTheory.Copula 2) (hC : C.IsExtremeValue) (hD : D.IsExtremeValue) :

C.LowerOrthantLE D ↔ ∀ (t : ↑unitInterval), 0 < t → t < 1 → Verification.copulaPickands D t ≤ Verification.copulaPickands C t

Theorem 3.4(i)-(ii), with a canonical Pickands function recovered from max-stability.

source

theorem Papers.AnsariRockel2024.extremeValue_schur_iff_pickands_of_ci (C D : ProbabilityTheory.Copula 2) (hC : C.IsExtremeValue) (hD : D.IsExtremeValue) (hCI : C.IsCI) (hDI : D.IsCI) :

C.SchurBothLE D ↔ ∀ (t : ↑unitInterval), 0 < t → t < 1 → Verification.copulaPickands D t ≤ Verification.copulaPickands C t

The Schur part of Theorem 3.4 under the independently required CI premise.

source

theorem Papers.AnsariRockel2024.extremeValue_schur_first_iff_pickands_of_ci (C D : ProbabilityTheory.Copula 2) (hC : C.IsExtremeValue) (hD : D.IsExtremeValue) (hCI : C.IsCI) (hDI : D.IsCI) :

C.SchurLE D ↔ ∀ (t : ↑unitInterval), 0 < t → t < 1 → Verification.copulaPickands D t ≤ Verification.copulaPickands C t

Theorem 3.4(iv), in the copula conditional-CDF form, under CI.

source

theorem Papers.AnsariRockel2024.extremeValue_schur_second_iff_pickands_of_ci (C D : ProbabilityTheory.Copula 2) (hC : C.IsExtremeValue) (hD : D.IsExtremeValue) (hCI : C.IsCI) (hDI : D.IsCI) :

C.transpose.SchurLE D.transpose ↔ ∀ (t : ↑unitInterval), 0 < t → t < 1 → Verification.copulaPickands D t ≤ Verification.copulaPickands C t

Theorem 3.4(v), with the conditioning coordinates exchanged, under CI.

source

theorem Papers.AnsariRockel2024.extremeValue_pickands_concordance_mono (C D : ProbabilityTheory.Copula 2) (hC : C.IsExtremeValue) (hD : D.IsExtremeValue) (h : ∀ (t : ↑unitInterval), 0 < t → t < 1 → Verification.copulaPickands D t ≤ Verification.copulaPickands C t) :

C.spearmanRho ≤ D.spearmanRho ∧ C.kendallTau ≤ D.kendallTau

Remark 3.5: Pickands order entails both classical concordance comparisons.

source

theorem Papers.AnsariRockel2024.extremeValue_pickands_xi_mono_of_ci (C D : ProbabilityTheory.Copula 2) (hC : C.IsExtremeValue) (hD : D.IsExtremeValue) (hCI : C.IsCI) (hDI : D.IsCI) (h : ∀ (t : ↑unitInterval), 0 < t → t < 1 → Verification.copulaPickands D t ≤ Verification.copulaPickands C t) :

C.chatterjeeXi ≤ D.chatterjeeXi ∧ C.transpose.chatterjeeXi ≤ D.transpose.chatterjeeXi

Remark 3.5: Pickands order entails both directional xi comparisons when CI is known.

source

theorem Papers.AnsariRockel2024.extremeValue_pickands_tail_mono (C D : ProbabilityTheory.Copula 2) (hC : C.IsExtremeValue) (hD : D.IsExtremeValue) (h : ∀ (t : ↑unitInterval), 0 < t → t < 1 → Verification.copulaPickands D t ≤ Verification.copulaPickands C t) :

((if C.extremalCoefficient = 1 then 1 else 0) ≤ if D.extremalCoefficient = 1 then 1 else 0) ∧ 2 - C.extremalCoefficient ≤ 2 - D.extremalCoefficient

Remark 3.5: both tail limits are ordered for max-stable copulas.

source

theorem Papers.AnsariRockel2024.extremeValue_pickands_representation (C : ProbabilityTheory.Copula 2) (hC : C.IsExtremeValue) (x y : ℝ) (hx : 0 ≤ x) (hy : 0 ≤ y) (hxy : 0 < x + y) :

C.cdf ![Verification.unitNegExp x hx, Verification.unitNegExp y hy] = Real.exp (-(x + y) * Verification.copulaPickands C ⟨y / (x + y), ⋯⟩)

The logarithmic-ray representation identifies the canonical function with the Pickands function in equation (3), including the axes.

source

theorem Papers.AnsariRockel2024.marshallOlkin_cdf (α β u v : ↑unitInterval) :

(ProbabilityTheory.Copula.marshallOlkin α β).cdf ![u, v] = min (↑u ^ (1 - ↑α) * ↑v) (↑u * ↑v ^ (1 - ↑β))

Table 1: the closed-square Marshall–Olkin formula.

source

theorem Papers.AnsariRockel2024.marshallOlkin_ci (α β : ↑unitInterval) :

(ProbabilityTheory.Copula.marshallOlkin α β).IsCI

Table 5: conditional increase in both directions, including singular parameters.

source

theorem Papers.AnsariRockel2024.marshallOlkin_orthant_mono {α β α' β' : ↑unitInterval} (ha : α ≤ α') (hb : β ≤ β') :

(ProbabilityTheory.Copula.marshallOlkin α β).LowerOrthantLE (ProbabilityTheory.Copula.marshallOlkin α' β')

Table 5: coordinatewise parameter increase raises the lower orthant probabilities.

source

theorem Papers.AnsariRockel2024.marshallOlkin_schur_mono {α β α' β' : ↑unitInterval} (ha : α ≤ α') (hb : β ≤ β') :

(ProbabilityTheory.Copula.marshallOlkin α β).SchurBothLE (ProbabilityTheory.Copula.marshallOlkin α' β')

Table 5: both directional Schur comparisons.

source

theorem Papers.AnsariRockel2024.cuadrasAuge_ci (δ : ↑unitInterval) :

(ProbabilityTheory.Copula.cuadrasAuge δ).IsCI

source

theorem Papers.AnsariRockel2024.cuadrasAuge_orthant_mono {δ η : ↑unitInterval} (h : δ ≤ η) :

(ProbabilityTheory.Copula.cuadrasAuge δ).LowerOrthantLE (ProbabilityTheory.Copula.cuadrasAuge η)

source

theorem Papers.AnsariRockel2024.cuadrasAuge_schur_mono {δ η : ↑unitInterval} (h : δ ≤ η) :

(ProbabilityTheory.Copula.cuadrasAuge δ).SchurBothLE (ProbabilityTheory.Copula.cuadrasAuge η)

source

theorem Papers.AnsariRockel2024.marshallOlkin_density_tp2 (α β : ↑unitInterval) :

(ProbabilityTheory.Copula.marshallOlkin α β).HasMTP2Density ↔ α = 0 ∨ β = 0

Table 5: a genuine Lebesgue TP2 density exists exactly on the independence axes.

source

theorem Papers.AnsariRockel2024.marshallOlkin_absolutelyContinuous (α β : ↑unitInterval) :

(ProbabilityTheory.Copula.marshallOlkin α β).toMeasure.AbsolutelyContinuous MeasureTheory.volume ↔ α = 0 ∨ β = 0

The singular component rules out any Lebesgue density off those axes.

source

theorem Papers.AnsariRockel2024.marshallOlkin_independence_axes (α : ↑unitInterval) :

ProbabilityTheory.Copula.marshallOlkin 0 α = ProbabilityTheory.Copula.independence 2 ∧ ProbabilityTheory.Copula.marshallOlkin α 0 = ProbabilityTheory.Copula.independence 2

Every zero-weight axis is independence, not only the origin.

source

theorem Papers.AnsariRockel2024.marshallOlkin_rho (α β : ↑unitInterval) :

(ProbabilityTheory.Copula.marshallOlkin α β).spearmanRho = 3 * ↑α * ↑β / (2 * ↑α + 2 * ↑β - ↑α * ↑β)

Table 6: Spearman rho for the full two-parameter Marshall–Olkin family.

source

theorem Papers.AnsariRockel2024.marshallOlkin_conditionalCDF (α β v : ↑unitInterval) (ha : 0 < ↑α) :

(fun (u : ↑unitInterval) => (ProbabilityTheory.Copula.marshallOlkin α β).conditionalCDF u v) =ᵐ[MeasureTheory.volume] fun (u : ↑unitInterval) => Verification.marshallOlkinConditional α β u v

Appendix A.5: the two-parameter conditional CDF, away from the shock curve.

source

theorem Papers.AnsariRockel2024.marshallOlkin_xi (α β : ↑unitInterval) :

(ProbabilityTheory.Copula.marshallOlkin α β).chatterjeeXi = 2 * ↑α ^ 2 * ↑β / (3 * ↑α + ↑β - 2 * ↑α * ↑β)

Table 6: Chatterjee xi for all Marshall–Olkin parameters, including singular laws.

source

theorem Papers.AnsariRockel2024.marshallOlkin_tau (α β : ↑unitInterval) :

(ProbabilityTheory.Copula.marshallOlkin α β).kendallTau = ↑α * ↑β / (↑α + ↑β - ↑α * ↑β)

Table 6: Kendall tau for the full two-parameter Marshall–Olkin family.

source

theorem Papers.AnsariRockel2024.extremeValue_pickands_bounds (C : ProbabilityTheory.Copula 2) (hC : C.IsExtremeValue) (t : ↑unitInterval) :

max (1 - ↑t) ↑t ≤ Verification.copulaPickands C t ∧ Verification.copulaPickands C t ≤ 1

source

theorem Papers.AnsariRockel2024.extremeValue_log_homogeneous (C : ProbabilityTheory.Copula 2) (hC : C.IsExtremeValue) (x y t : ℝ) (hx : 0 ≤ x) (hy : 0 ≤ y) (ht : 0 ≤ t) :

Verification.extremeValueLog C (t * x) (t * y) ⋯ ⋯ = t * Verification.extremeValueLog C x y hx hy

source

theorem Papers.AnsariRockel2024.extremeValue_log_submodular (C : ProbabilityTheory.Copula 2) (hC : C.IsExtremeValue) {x₁ x₂ y₁ y₂ : ℝ} (hx : 0 ≤ x₁) (hy : 0 ≤ y₁) (hxx : x₁ ≤ x₂) (hyy : y₁ ≤ y₂) :

Verification.extremeValueLog C x₁ y₁ hx hy + Verification.extremeValueLog C x₂ y₂ ⋯ ⋯ ≤ Verification.extremeValueLog C x₁ y₂ hx ⋯ + Verification.extremeValueLog C x₂ y₁ ⋯ hy

source

theorem Papers.AnsariRockel2024.extremeValue_log_increment_first (C : ProbabilityTheory.Copula 2) (hC : C.IsExtremeValue) {x₁ x₂ y : ℝ} (hx : 0 ≤ x₁) (hy : 0 ≤ y) (hxx : x₁ ≤ x₂) :

0 ≤ Verification.extremeValueLog C x₂ y ⋯ hy - Verification.extremeValueLog C x₁ y hx hy ∧ Verification.extremeValueLog C x₂ y ⋯ hy - Verification.extremeValueLog C x₁ y hx hy ≤ x₂ - x₁

source

theorem Papers.AnsariRockel2024.extremeValue_log_increment_second (C : ProbabilityTheory.Copula 2) (hC : C.IsExtremeValue) {x y₁ y₂ : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y₁) (hyy : y₁ ≤ y₂) :

0 ≤ Verification.extremeValueLog C x y₂ hx ⋯ - Verification.extremeValueLog C x y₁ hx hy ∧ Verification.extremeValueLog C x y₂ hx ⋯ - Verification.extremeValueLog C x y₁ hx hy ≤ y₂ - y₁

source

theorem Papers.AnsariRockel2024.extremeValue_log_section_convex (C : ProbabilityTheory.Copula 2) (hC : C.IsExtremeValue) (y : ℝ) (hy : 0 ≤ y) :

ConvexOn ℝ (Set.Ioi 0) (Verification.extremeValueLogSection C y hy)

source

theorem Papers.AnsariRockel2024.extremeValue_ci (C : ProbabilityTheory.Copula 2) (hC : C.IsExtremeValue) :

C.IsCI

Every max-stable bivariate copula is conditionally increasing, without a density assumption.

source

theorem Papers.AnsariRockel2024.extremeValue_schur_iff_pickands (C D : ProbabilityTheory.Copula 2) (hC : C.IsExtremeValue) (hD : D.IsExtremeValue) :

C.SchurBothLE D ↔ ∀ (t : ↑unitInterval), 0 < t → t < 1 → Verification.copulaPickands D t ≤ Verification.copulaPickands C t

Theorem 3.4(iii), without a separate CI hypothesis.

source

theorem Papers.AnsariRockel2024.extremeValue_schur_first_iff_pickands (C D : ProbabilityTheory.Copula 2) (hC : C.IsExtremeValue) (hD : D.IsExtremeValue) :

C.SchurLE D ↔ ∀ (t : ↑unitInterval), 0 < t → t < 1 → Verification.copulaPickands D t ≤ Verification.copulaPickands C t

Theorem 3.4(iv), without a separate CI hypothesis.

source

theorem Papers.AnsariRockel2024.extremeValue_schur_second_iff_pickands (C D : ProbabilityTheory.Copula 2) (hC : C.IsExtremeValue) (hD : D.IsExtremeValue) :

C.transpose.SchurLE D.transpose ↔ ∀ (t : ↑unitInterval), 0 < t → t < 1 → Verification.copulaPickands D t ≤ Verification.copulaPickands C t

Theorem 3.4(v), without a separate CI hypothesis.

source

theorem Papers.AnsariRockel2024.extremeValue_pickands_xi_mono (C D : ProbabilityTheory.Copula 2) (hC : C.IsExtremeValue) (hD : D.IsExtremeValue) (h : ∀ (t : ↑unitInterval), 0 < t → t < 1 → Verification.copulaPickands D t ≤ Verification.copulaPickands C t) :

C.chatterjeeXi ≤ D.chatterjeeXi ∧ C.transpose.chatterjeeXi ≤ D.transpose.chatterjeeXi

Remark 3.5: both directional xi comparisons for arbitrary extreme-value copulas.

source

theorem Papers.AnsariRockel2024.extremeValue_pickands_real_coe (C : ProbabilityTheory.Copula 2) (hC : C.IsExtremeValue) (t : ↑unitInterval) :

Verification.copulaPickandsReal C ↑t = Verification.copulaPickands C t

The real-coordinate extension agrees with the canonical Pickands function on its domain.

source

theorem Papers.AnsariRockel2024.extremeValue_pickands_convex (C : ProbabilityTheory.Copula 2) (hC : C.IsExtremeValue) :

ConvexOn ℝ (Set.Icc 0 1) (Verification.copulaPickandsReal C)

Section 2.1.2: convexity follows from the actual max-stable copula.

Documentation

Papers.AnsariRockel2024.ExtremeValueOrders

Extreme-value CDF order and explicit monotone families #