← Copula mathematical handbook

Blomqvist's beta of Nelsen's Table 4.1, families 9 to 22

Continuation of Copula.Archimedean.BlomqvistTable: β = 4 C(1/2, 1/2) - 1 for the families 4.2.9, 10, 11, 13, 16, 17, 18, 19, 20, 21, 22 of Nelsen, An Introduction to Copulas, second edition, Table 4.1 (families 12, 14, 15 are in the first file). In every case the value is elementary.

theorem ProbabilityTheory.Copula.blomqvistBeta_nelsen9 (θ : ℝ) (hθ : 0 < θ) (h1 : θ ≤ 1) : (nelsen9 θ hθ h1).blomqvistBeta = Real.exp (-(θ * Real.log 2 ^ 2)) - 1

Nelsen 9 (0 < θ ≤ 1): β = exp (-θ (log 2)^2) - 1.

theorem ProbabilityTheory.Copula.blomqvistBeta_nelsen10 (θ : ℝ) (hθ : 0 < θ) (h1 : θ ≤ 1) : (nelsen10 θ hθ h1).blomqvistBeta = ((1 + (1 - (2 ^ θ)⁻¹) ^ 2) ^ θ⁻¹)⁻¹ - 1

Nelsen 10 (0 < θ ≤ 1): β = (1 + (1 - 2^(-θ))^2)^(-1/θ) - 1.

theorem ProbabilityTheory.Copula.blomqvistBeta_nelsen11 (θ : ℝ) (hθ : 0 < θ) (h2 : θ ≤ 1 / 2) : (nelsen11 θ hθ h2).blomqvistBeta = 4 * (4 * (2 ^ θ)⁻¹ - (2 ^ θ)⁻¹ ^ 2 - 2) ^ θ⁻¹ - 1

Nelsen 11 (0 < θ ≤ 1/2): with a = 2^(-θ), β = 4 (4a - a^2 - 2)^(1/θ) - 1.

theorem ProbabilityTheory.Copula.blomqvistBeta_nelsen13 (θ : ℝ) (hθ : 0 < θ) : (nelsen13 θ hθ).blomqvistBeta = 4 * Real.exp (1 - (2 * (1 + Real.log 2) ^ θ - 1) ^ θ⁻¹) - 1

Nelsen 13 (θ > 0): β = 4 exp (1 - (2 (1 + log 2)^θ - 1)^(1/θ)) - 1.

theorem ProbabilityTheory.Copula.blomqvistBeta_nelsen16 (θ : ℝ) (hθ : 0 ≤ θ) : (nelsen16 θ hθ).blomqvistBeta = 2 * (√(9 * θ ^ 2 + 4 * θ) - 3 * θ) - 1

Nelsen 16 (θ ≥ 0): β = 2 (sqrt (9θ² + 4θ) - 3θ) - 1.

theorem ProbabilityTheory.Copula.blomqvistBeta_nelsen17 (θ : ℝ) (hθ : θ ≠ 0) : (nelsen17 θ hθ).blomqvistBeta = 4 * ((1 + ((3 / 2) ^ (-θ) - 1) ^ 2 / (2 ^ (-θ) - 1)) ^ (-θ⁻¹) - 1) - 1

Nelsen 17 (θ ≠ 0): β = 4 ((1 + ((3/2)^(-θ) - 1)^2 / (2^(-θ) - 1))^(-1/θ) - 1) - 1.

theorem ProbabilityTheory.Copula.blomqvistBeta_nelsen18 (θ : ℝ) (hθ : 2 ≤ θ) : (nelsen18 θ hθ).blomqvistBeta = (2 * θ - 3 * Real.log 2) / (2 * θ - Real.log 2)

Nelsen 18 (θ ≥ 2): β = (2θ - 3 log 2) / (2θ - log 2).

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

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

theorem ProbabilityTheory.Copula.blomqvistBeta_nelsen20 (θ : ℝ) (hθ : 0 < θ) : (nelsen20 θ hθ).blomqvistBeta = 4 * Real.log (2 * Real.exp (2 ^ θ) - Real.exp 1) ^ (-θ⁻¹) - 1

Nelsen 20 (θ > 0): β = 4 (log (2 exp (2^θ) - e))^(-1/θ) - 1.

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

Nelsen 21 (θ ≥ 1): with p = (1 - 2^(-θ))^(1/θ), β = 3 - 4 (1 - (2p - 1)^θ)^(1/θ).

theorem ProbabilityTheory.Copula.blomqvistBeta_nelsen22 (θ : ℝ) (hθ : 0 < θ) (h1 : θ ≤ 1) : (nelsen22 θ hθ h1).blomqvistBeta = if 2 * (1 - (2 ^ θ)⁻¹) ^ 2 ≤ 1 then 4 * (1 - 2 * (1 - (2 ^ θ)⁻¹) * √(1 - (1 - (2 ^ θ)⁻¹) ^ 2)) ^ θ⁻¹ - 1 else -1

Nelsen 22 (0 < θ ≤ 1): with b = 1 - 2^(-θ), β = 4 (1 - 2 b sqrt (1 - b^2))^(1/θ) - 1 if 2 b^2 ≤ 1 and β = -1 otherwise.