← Copula mathematical handbook

Nelsen's family 22

Nelsen, An Introduction to Copulas, second edition, Table 4.1, number 22 (Section 4.2): generator φ(t) = arcsin (1 - t^θ) for 0 < θ ≤ 1.

The generator is non-strict (φ(0) = π/2). At θ = 1 the pseudo-inverse is ψ₁(s) = 1 - sin (min s (π/2)), convex because sin is concave on [0, π]; it is built with BivariateGenerator.ofClamp. For general θ the pseudo-inverse is ψ₁^(1/θ), the inner power BivariateGenerator.innerPower with exponent 1/θ ≥ 1, so no further convexity argument is needed.

Correction of the printed formula. With a = 1 - u^θ and b = 1 - v^θ, Table 4.1 prints C(u, v) = max ((1 - a √(1 - b²) - b √(1 - a²))^(1/θ)) 0. This is only correct where φ(u) + φ(v) = arcsin a + arcsin b ≤ π/2, which is equivalent to a² + b² ≤ 1. Beyond that region the copula vanishes, while the printed expression is positive (for small u = v it tends to 1, exceeding min(u, v)). The theorem cdf_nelsen22 states the correct formula: C(u, v) = (1 - a √(1 - b²) - b √(1 - a²))^(1/θ) if a² + b² ≤ 1, and 0 otherwise.

noncomputable def ProbabilityTheory.Copula.nelsen22BaseGenerator : BivariateGenerator

The clamped pseudo-inverse s ↦ 1 - sin (min s (π/2)) of Nelsen's family 22 at θ = 1. Its generator is u ↦ arcsin (1 - u).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def ProbabilityTheory.Copula.nelsen22Generator (θ : ℝ) (hθ : 0 < θ) (h1 : θ ≤ 1) : BivariateGenerator

The pseudo-inverse s ↦ (1 - sin (min s (π/2)))^(1/θ) of Nelsen's family 22, for 0 < θ ≤ 1: the 1/θ-th inner power of nelsen22BaseGenerator.

Equations

• ProbabilityTheory.Copula.nelsen22Generator θ hθ h1 = ProbabilityTheory.Copula.nelsen22BaseGenerator.innerPower θ⁻¹ ⋯

noncomputable def ProbabilityTheory.Copula.nelsen22 (θ : ℝ) (hθ : 0 < θ) (h1 : θ ≤ 1) : Copula 2

Nelsen's family 22 for 0 < θ ≤ 1.

Equations

• ProbabilityTheory.Copula.nelsen22 θ hθ h1 = (ProbabilityTheory.Copula.nelsen22Generator θ hθ h1).copula

theorem ProbabilityTheory.Copula.isArchimedean_nelsen22 (θ : ℝ) (hθ : 0 < θ) (h1 : θ ≤ 1) : (nelsen22 θ hθ h1).IsArchimedean

theorem ProbabilityTheory.Copula.nelsen22Generator_invFun (θ : ℝ) (hθ : 0 < θ) (h1 : θ ≤ 1) (u : ↑unitInterval) : (nelsen22Generator θ hθ h1).invFun u = Real.arcsin (1 - ↑u ^ θ)

The generator of Nelsen's family 22 is u ↦ arcsin (1 - u^θ).

theorem ProbabilityTheory.Copula.nelsen22Generator_toFun (θ : ℝ) (hθ : 0 < θ) (h1 : θ ≤ 1) (s : ℝ) : (nelsen22Generator θ hθ h1).toFun s = (1 - Real.sin (min s (Real.pi / 2))) ^ θ⁻¹

The pseudo-inverse of family 22 is s ↦ (1 - sin (min s (π/2)))^(1/θ).

theorem ProbabilityTheory.Copula.arcsin_add_arcsin_le_pi_div_two_iff {a b : ℝ} (ha0 : 0 ≤ a) (ha1 : a ≤ 1) (hb0 : 0 ≤ b) (hb1 : b ≤ 1) : Real.arcsin a + Real.arcsin b ≤ Real.pi / 2 ↔ a ^ 2 + b ^ 2 ≤ 1

For a, b ∈ [0, 1]: arcsin a + arcsin b ≤ π/2 ↔ a² + b² ≤ 1.

theorem ProbabilityTheory.Copula.cdf_nelsen22 (θ : ℝ) (hθ : 0 < θ) (h1 : θ ≤ 1) (u v : ↑unitInterval) (hu : u ≠ 0) (hv : v ≠ 0) : (nelsen22 θ hθ h1).cdf ![u, v] = if (1 - ↑u ^ θ) ^ 2 + (1 - ↑v ^ θ) ^ 2 ≤ 1 then (1 - (1 - ↑u ^ θ) * √(1 - (1 - ↑v ^ θ) ^ 2) - (1 - ↑v ^ θ) * √(1 - (1 - ↑u ^ θ) ^ 2)) ^ θ⁻¹ else 0

The CDF of Nelsen's family 22 on positive coordinates, with a = 1 - u^θ, b = 1 - v^θ: C(u, v) = (1 - a √(1 - b²) - b √(1 - a²))^(1/θ) if a² + b² ≤ 1 and 0 otherwise. (Nelsen's printed formula omits the case distinction; see the module docstring.)

theorem ProbabilityTheory.Copula.nelsen22_cdf_full (θ : ℝ) (hθ : 0 < θ) (h1 : θ ≤ 1) (u v : ↑unitInterval) : (nelsen22 θ hθ h1).cdf ![u, v] = if u = 0 ∨ v = 0 then 0 else if (1 - ↑u ^ θ) ^ 2 + (1 - ↑v ^ θ) ^ 2 ≤ 1 then (1 - (1 - ↑u ^ θ) * √(1 - (1 - ↑v ^ θ) ^ 2) - (1 - ↑v ^ θ) * √(1 - (1 - ↑u ^ θ) ^ 2)) ^ θ⁻¹ else 0

Nelsen's family 22 on the whole closed unit square, with grounded zero axes.