← Mathematical handbook

Tables 5 and A.4: Frechet and Mardia dependence classifications

The valid Frechet simplex is a,b>=0 and a+b<=1. Mardia has W weight theta^2(1-theta)/2. Its independence parameter zero belongs to both CI and CD. Density TP2 is interpreted literally as existence of a Lebesgue TP2 density; positive singular weights rule out even absolute continuity.

theorem Papers.AnsariRockel2024.frechet_ci_iff (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b ≤ 1) : (ProbabilityTheory.Copula.frechet a b ha hb hab).IsCI ↔ b = 0

theorem Papers.AnsariRockel2024.frechet_cd_iff (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b ≤ 1) : (ProbabilityTheory.Copula.frechet a b ha hb hab).IsCD ↔ a = 0

theorem Papers.AnsariRockel2024.frechet_absolutelyContinuous_iff (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b ≤ 1) : (ProbabilityTheory.Copula.frechet a b ha hb hab).toMeasure.AbsolutelyContinuous MeasureTheory.volume ↔ a = 0 ∧ b = 0

theorem Papers.AnsariRockel2024.frechet_density_tp2_iff (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b ≤ 1) : (ProbabilityTheory.Copula.frechet a b ha hb hab).HasMTP2Density ↔ a = 0 ∧ b = 0

theorem Papers.AnsariRockel2024.mardia_ci_iff (θ : ℝ) (hθ : |θ| ≤ 1) : (ProbabilityTheory.Copula.mardia θ hθ).IsCI ↔ θ = 0 ∨ θ = 1

theorem Papers.AnsariRockel2024.mardia_cd_iff (θ : ℝ) (hθ : |θ| ≤ 1) : (ProbabilityTheory.Copula.mardia θ hθ).IsCD ↔ θ = 0 ∨ θ = -1

theorem Papers.AnsariRockel2024.mardia_absolutelyContinuous_iff (θ : ℝ) (hθ : |θ| ≤ 1) : (ProbabilityTheory.Copula.mardia θ hθ).toMeasure.AbsolutelyContinuous MeasureTheory.volume ↔ θ = 0

theorem Papers.AnsariRockel2024.mardia_density_tp2_iff (θ : ℝ) (hθ : |θ| ≤ 1) : (ProbabilityTheory.Copula.mardia θ hθ).HasMTP2Density ↔ θ = 0

theorem Papers.AnsariRockel2024.mardia_not_lowerOrthant_ordered : ¬(ProbabilityTheory.Copula.mardia (1 / 2) ⋯).LowerOrthantLE (ProbabilityTheory.Copula.mardia 0 ⋯) ∧ ¬(ProbabilityTheory.Copula.mardia 0 ⋯).LowerOrthantLE (ProbabilityTheory.Copula.mardia (1 / 2) ⋯)