← Mathematical handbook

Exact dependence classifications of Frechet mixtures

theorem ProbabilityTheory.Copula.frechet_exchangeable (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b ≤ 1) : (frechet a b ha hb hab).IsExchangeable

theorem ProbabilityTheory.Copula.frechet_si_iff (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b ≤ 1) : (frechet a b ha hb hab).IsSI ↔ b = 0

theorem ProbabilityTheory.Copula.frechet_sd_iff (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b ≤ 1) : (frechet a b ha hb hab).IsSD ↔ a = 0

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

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

theorem ProbabilityTheory.Copula.frechet_measure (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b ≤ 1) : (frechet a b ha hb hab).toMeasure = ENNReal.ofReal a • (comonotonic 2).toMeasure + ENNReal.ofReal b • countermonotonic.toMeasure + ENNReal.ofReal (1 - a - b) • (independence 2).toMeasure

Measure-level identity, including singular component weights.

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

A Frechet mixture is absolutely continuous exactly when both singular weights vanish.

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

Density TP2 is possible only at independence, not at the singular M or W endpoints.

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

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

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

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

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

A concrete incomparable pair proves the source's lack of parameter ordering.