← Copula mathematical handbook

Blomqvist's beta of the classical Archimedean families

Blomqvist's beta is β = 4 C(1/2, 1/2) - 1, so for every family with an explicit CDF it is obtained by evaluating the CDF at the centre of the unit square. This file treats the families of Nelsen, An Introduction to Copulas, second edition, Table 4.1, numbers 1, 2, 3, 5, 6, 7, 8, 12, 14, 15 (Gumbel, number 4, is in Copula.Rank.PowerDiagonal); the remaining families are in Copula.Archimedean.BlomqvistTableN.

theorem ProbabilityTheory.Copula.BlomqvistTable.half_val : ↑unitHalf = 1 / 2

theorem ProbabilityTheory.Copula.BlomqvistTable.half_ne_zero : unitHalf ≠ 0

theorem ProbabilityTheory.Copula.BlomqvistTable.not_zero_or : ¬(unitHalf = 0 ∨ unitHalf = 0)

theorem ProbabilityTheory.Copula.BlomqvistTable.half_rpow_neg (θ : ℝ) : (1 / 2) ^ (-θ) = 2 ^ θ

theorem ProbabilityTheory.Copula.BlomqvistTable.half_rpow (θ : ℝ) : (1 / 2) ^ θ = (2 ^ θ)⁻¹

theorem ProbabilityTheory.Copula.blomqvistBeta_clayton (θ : ℝ) (hθ : 0 < θ) : (clayton 2 θ hθ).blomqvistBeta = 4 * (2 ^ (θ + 1) - 1) ^ (-1 / θ) - 1

Clayton, θ > 0: β = 4 (2^(θ+1) - 1)^(-1/θ) - 1.

theorem ProbabilityTheory.Copula.blomqvistBeta_claytonNegative (θ : ℝ) (hθ : -1 ≤ θ) (hn : θ < 0) : (claytonNegative θ hθ hn).blomqvistBeta = 4 * (2 ^ (θ + 1) - 1) ^ (-1 / θ) - 1

Clayton, -1 ≤ θ < 0: the same formula β = 4 (2^(θ+1) - 1)^(-1/θ) - 1.

theorem ProbabilityTheory.Copula.two_half_rpow_inv (θ : ℝ) (hθ : 0 < θ) : ((1 - 1 / 2) ^ θ + (1 - 1 / 2) ^ θ) ^ θ⁻¹ = 2 ^ θ⁻¹ / 2

Two equal terms (1/2)^θ under a θ-th root: (2 (1/2)^θ)^(1/θ) = 2^(1/θ) / 2.

theorem ProbabilityTheory.Copula.blomqvistBeta_nelsen2 (θ : ℝ) (hθ : 1 ≤ θ) : (nelsen2 θ hθ).blomqvistBeta = 3 - 2 ^ (θ⁻¹ + 1)

Nelsen 2 (θ ≥ 1): β = 3 - 2^(1/θ + 1).

theorem ProbabilityTheory.Copula.blomqvistBeta_amh (θ : ℝ) (hmin : -1 ≤ θ) (hmax : θ ≤ 1) : (amh θ hmin hmax).blomqvistBeta = θ / (4 - θ)

Ali--Mikhail--Haq (-1 ≤ θ ≤ 1): β = θ / (4 - θ).

theorem ProbabilityTheory.Copula.blomqvistBeta_frank (θ : ℝ) (hθ : 0 < θ) : (frank θ hθ).blomqvistBeta = 4 * Real.log ((1 + Real.exp (θ / 2)) / 2) / θ - 1

Frank (θ > 0): β = 4 log ((1 + e^(θ/2)) / 2) / θ - 1.

theorem ProbabilityTheory.Copula.blomqvistBeta_frankNegative (θ : ℝ) (hθ : θ < 0) : (frankNegative θ hθ).blomqvistBeta = 1 + 4 * Real.log ((1 + Real.exp (-θ / 2)) / 2) / θ

Frank (θ < 0): β = 1 + 4 log ((1 + e^(-θ/2)) / 2) / θ.

theorem ProbabilityTheory.Copula.blomqvistBeta_joe (θ : ℝ) (hθ : 1 ≤ θ) : (joe θ hθ).blomqvistBeta = 3 - 2 * (2 - (2 ^ θ)⁻¹) ^ θ⁻¹

Joe (θ ≥ 1): β = 3 - 2 (2 - 2^(-θ))^(1/θ).

theorem ProbabilityTheory.Copula.blomqvistBeta_nelsen7 (θ : ↑unitInterval) : (nelsen7 θ).blomqvistBeta = ↑θ - 1

Nelsen 7 (θ ∈ [0, 1]): β = θ - 1.

theorem ProbabilityTheory.Copula.blomqvistBeta_nelsen8 (θ : ℝ) (hθ : 1 ≤ θ) : (nelsen8 θ hθ).blomqvistBeta = (θ - 3) / (3 * θ - 1)

Nelsen 8 (θ ≥ 1): β = (θ - 3) / (3θ - 1).

theorem ProbabilityTheory.Copula.two_rpow_inv_mul (θ x : ℝ) (hθ : 0 < θ) (hx : 0 ≤ x) : (x ^ θ + x ^ θ) ^ θ⁻¹ = 2 ^ θ⁻¹ * x

(x^θ + x^θ)^(1/θ) = 2^(1/θ) x for x ≥ 0.

theorem ProbabilityTheory.Copula.blomqvistBeta_nelsen12 (θ : ℝ) (hθ : 1 ≤ θ) : (nelsen12 θ hθ).blomqvistBeta = 4 * (1 + 2 ^ θ⁻¹)⁻¹ - 1

Nelsen 12 (θ ≥ 1): β = 4 / (1 + 2^(1/θ)) - 1.

theorem ProbabilityTheory.Copula.blomqvistBeta_nelsen14 (θ : ℝ) (hθ : 1 ≤ θ) : (nelsen14 θ hθ).blomqvistBeta = 4 * (1 + 2 ^ θ⁻¹ * (2 ^ θ⁻¹ - 1)) ^ (-θ) - 1

Nelsen 14 (θ ≥ 1): with q = 2^(1/θ), β = 4 (1 + q (q - 1))^(-θ) - 1.

theorem ProbabilityTheory.Copula.blomqvistBeta_genestGhoudi (θ : ℝ) (hθ : 1 ≤ θ) : (genestGhoudi θ hθ).blomqvistBeta = 4 * (2 - 2 ^ θ⁻¹) ^ θ - 1

Nelsen 15 (Genest--Ghoudi, θ ≥ 1): β = 4 (2 - 2^(1/θ))^θ - 1.