Papers.AnsariRockel2024.Dependence

← Mathematical handbook

source

theorem Papers.AnsariRockel2024.amh_pqd_iff (θ : ℝ) (hmin : -1 ≤ θ) (hmax : θ ≤ 1) :

(ProbabilityTheory.Copula.amh θ hmin hmax).IsPQD ↔ 0 ≤ θ

Table 3: AMH is positively quadrant dependent exactly for nonnegative θ.

source

theorem Papers.AnsariRockel2024.amh_nqd_iff (θ : ℝ) (hmin : -1 ≤ θ) (hmax : θ ≤ 1) :

(ProbabilityTheory.Copula.amh θ hmin hmax).IsNQD ↔ θ ≤ 0

Table 3: AMH is negatively quadrant dependent exactly for nonpositive θ.

source

theorem Papers.AnsariRockel2024.amh_tails_lt_one (θ : ℝ) (hmin : -1 ≤ θ) (hmax : θ ≤ 1) (hθ : θ < 1) :

(ProbabilityTheory.Copula.amh θ hmin hmax).HasLowerTailDependence 0 ∧ (ProbabilityTheory.Copula.amh θ hmin hmax).HasUpperTailDependence 0

Corrected Table 3 AMH tail pair for every parameter below one.

source

theorem Papers.AnsariRockel2024.amh_tails_one :

(ProbabilityTheory.Copula.amh 1 ⋯ ⋯).HasLowerTailDependence (1 / 2) ∧ (ProbabilityTheory.Copula.amh 1 ⋯ ⋯).HasUpperTailDependence 0

Corrected Table 3 AMH endpoint: Clayton(1) has lower-tail coefficient 1/2.

source

theorem Papers.AnsariRockel2024.amh_lowerOrthant_iff {θ η : ℝ} (hθmin : -1 ≤ θ) (hθmax : θ ≤ 1) (hηmin : -1 ≤ η) (hηmax : η ≤ 1) :

(ProbabilityTheory.Copula.amh θ hθmin hθmax).LowerOrthantLE (ProbabilityTheory.Copula.amh η hηmin hηmax) ↔ θ ≤ η

Table 3: exact lower-orthant parameter ordering for the AMH family.

source

theorem Papers.AnsariRockel2024.amh_ci_iff (θ : ℝ) (hmin : -1 ≤ θ) (hmax : θ ≤ 1) :

(ProbabilityTheory.Copula.amh θ hmin hmax).IsCI ↔ 0 ≤ θ

Table 3: AMH is conditionally increasing exactly for nonnegative θ.

source

theorem Papers.AnsariRockel2024.amh_cd_iff (θ : ℝ) (hmin : -1 ≤ θ) (hmax : θ ≤ 1) :

(ProbabilityTheory.Copula.amh θ hmin hmax).IsCD ↔ θ ≤ 0

Table 3: AMH is conditionally decreasing exactly for nonpositive θ.

source

theorem Papers.AnsariRockel2024.fgm_ci (θ : ℝ) (hθ : |θ| ≤ 1) :

(ProbabilityTheory.Copula.fgm θ hθ).IsCI ↔ 0 ≤ θ

arXiv:2310.17307v3, Table 5 / Appendix A.4.1: FGM CI. See COVERAGE.md for conventions.

source

theorem Papers.AnsariRockel2024.fgm_cd (θ : ℝ) (hθ : |θ| ≤ 1) :

(ProbabilityTheory.Copula.fgm θ hθ).IsCD ↔ θ ≤ 0

arXiv:2310.17307v3, Table 5 / Appendix A.4.1: FGM CD. See COVERAGE.md for conventions.

source

theorem Papers.AnsariRockel2024.fgm_lowerOrthant {θ η : ℝ} (hθ : |θ| ≤ 1) (hη : |η| ≤ 1) :

(ProbabilityTheory.Copula.fgm θ hθ).LowerOrthantLE (ProbabilityTheory.Copula.fgm η hη) ↔ θ ≤ η

arXiv:2310.17307v3, Table 5 / Appendix A.4.2: FGM lower orthant order. See COVERAGE.md for conventions.

source

theorem Papers.AnsariRockel2024.fgm_tails (θ : ℝ) (hθ : |θ| ≤ 1) :

(ProbabilityTheory.Copula.fgm θ hθ).HasLowerTailDependence 0 ∧ (ProbabilityTheory.Copula.fgm θ hθ).HasUpperTailDependence 0

arXiv:2310.17307v3, Table 5 / Appendix A.4.3: FGM lower and upper tails. See COVERAGE.md for conventions.

source

theorem Papers.AnsariRockel2024.frechet_tails (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b ≤ 1) :

(ProbabilityTheory.Copula.frechet a b ha hb hab).HasLowerTailDependence a ∧ (ProbabilityTheory.Copula.frechet a b ha hb hab).HasUpperTailDependence a

arXiv:2310.17307v3, Table 5 / Appendix A.4.3: Frechet tails. See COVERAGE.md for conventions.

source

theorem Papers.AnsariRockel2024.mardia_tails (θ : ℝ) (hθ : |θ| ≤ 1) :

(ProbabilityTheory.Copula.mardia θ hθ).HasLowerTailDependence (θ ^ 2 * (1 + θ) / 2) ∧ (ProbabilityTheory.Copula.mardia θ hθ).HasUpperTailDependence (θ ^ 2 * (1 + θ) / 2)

arXiv:2310.17307v3, Table 5 / Appendix A.4.3: Mardia tails. See COVERAGE.md for conventions.