← Mathematical handbook

Further Tables 3 and 5: tail limits and parameter orders

These statements connect the article's cells to the pinned library proofs. Both tails include existence of the limit and all admitted finite parameters. The Frechet order corrects the source's direction for the W weight.

theorem Papers.AnsariRockel2024.gumbel_tails (θ : ℝ) (hθ : 1 ≤ θ) : (ProbabilityTheory.Copula.gumbel θ hθ).HasLowerTailDependence 0 ∧ (ProbabilityTheory.Copula.gumbel θ hθ).HasUpperTailDependence (2 - 2 ^ θ⁻¹)

theorem Papers.AnsariRockel2024.joe_tails (θ : ℝ) (hθ : 1 ≤ θ) : (ProbabilityTheory.Copula.joe θ hθ).HasLowerTailDependence 0 ∧ (ProbabilityTheory.Copula.joe θ hθ).HasUpperTailDependence (2 - 2 ^ θ⁻¹)

Table 3: Joe has its stated lower and upper tail coefficients.

theorem Papers.AnsariRockel2024.nelsen8_tails (θ : ℝ) (hθ : 1 ≤ θ) : (ProbabilityTheory.Copula.nelsen8 θ hθ).HasLowerTailDependence 0 ∧ (ProbabilityTheory.Copula.nelsen8 θ hθ).HasUpperTailDependence 0

Table 3: Nelsen 8 has zero lower and upper tail coefficients.

theorem Papers.AnsariRockel2024.nelsen8_lowerOrthant {θ η : ℝ} (hθ : 1 ≤ θ) (hη : 1 ≤ η) (hθη : θ ≤ η) : (ProbabilityTheory.Copula.nelsen8 θ hθ).LowerOrthantLE (ProbabilityTheory.Copula.nelsen8 η hη)

Table 3: Nelsen 8 increases in lower-orthant order for θ ≥ 1.

theorem Papers.AnsariRockel2024.nelsen2_tails (θ : ℝ) (hθ : 1 ≤ θ) : (ProbabilityTheory.Copula.nelsen2 θ hθ).HasLowerTailDependence 0 ∧ (ProbabilityTheory.Copula.nelsen2 θ hθ).HasUpperTailDependence (2 - 2 ^ θ⁻¹)

Table 3: Nelsen 2 has the stated lower and upper tail coefficients.

theorem Papers.AnsariRockel2024.marshallOlkin_tails (α β : ↑unitInterval) : (ProbabilityTheory.Copula.marshallOlkin α β).HasLowerTailDependence (if α = 1 ∧ β = 1 then 1 else 0) ∧ (ProbabilityTheory.Copula.marshallOlkin α β).HasUpperTailDependence (min ↑α ↑β)

theorem Papers.AnsariRockel2024.cuadrasAuge_tails (δ : ↑unitInterval) : (ProbabilityTheory.Copula.cuadrasAuge δ).HasLowerTailDependence (if δ = 1 then 1 else 0) ∧ (ProbabilityTheory.Copula.cuadrasAuge δ).HasUpperTailDependence ↑δ

theorem Papers.AnsariRockel2024.tawn_tails (θ : ℝ) (hθ : 1 ≤ θ) (α β : ↑unitInterval) : (ProbabilityTheory.Copula.tawn θ hθ α β).HasLowerTailDependence 0 ∧ (ProbabilityTheory.Copula.tawn θ hθ α β).HasUpperTailDependence (↑α + ↑β - (↑α ^ θ + ↑β ^ θ) ^ θ⁻¹)

theorem Papers.AnsariRockel2024.fgm_schur_iff (θ η : ℝ) (hθ : |θ| ≤ 1) (hη : |η| ≤ 1) : (ProbabilityTheory.Copula.fgm θ hθ).SchurBothLE (ProbabilityTheory.Copula.fgm η hη) ↔ |θ| ≤ |η|

Two-direction Schur comparison on the entire signed FGM parameter interval.

theorem Papers.AnsariRockel2024.frechet_parameter_order (a b a' b' : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b ≤ 1) (ha' : 0 ≤ a') (hb' : 0 ≤ b') (hab' : a' + b' ≤ 1) (haa : a ≤ a') (hbb : b' ≤ b) : (ProbabilityTheory.Copula.frechet a b ha hb hab).LowerOrthantLE (ProbabilityTheory.Copula.frechet a' b' ha' hb' hab')

Increasing M's weight and decreasing W's weight increases the copula in LO order.

theorem Papers.AnsariRockel2024.frechet_order_counterexample : ¬(ProbabilityTheory.Copula.frechet 0 0 ⋯ ⋯ ⋯).LowerOrthantLE (ProbabilityTheory.Copula.frechet 0 1 ⋯ ⋯ ⋯)

The source's increasing-in-W-weight direction fails already at the endpoints.