← Copula mathematical handbook

Spearman's rho of Nelsen's family 2

Nelsen's family 2 is C(u, v) = max (0, 1 - ((1-u)^θ + (1-v)^θ)^(1/θ)), θ ≥ 1. Writing x = 1-u, y = 1-v, we have C = (1 - ‖(x, y)‖_θ)₊, the cone over the ℓ^θ unit ball (SpearmanNelsen2.cone). By the layer-cake formula and the volume of the ℓ^θ unit ball of the plane (Mathlib: MeasureTheory.volume_sum_rpow_lt) the integral of the cone over the plane is V / 3 with V = (2 Γ(1 + 1/θ))² / Γ(1 + 2/θ); by symmetry the quadrant carries a quarter of it, so ∬ C = V / 12 and

ρ = 4 Γ(1 + 1/θ)² / Γ(1 + 2/θ) - 3 (spearmanRho_nelsen2).

For θ = 1 this is -1 (the copula is W), and ρ → 1 as θ → ∞.

noncomputable def ProbabilityTheory.Copula.SpearmanNelsen2.cone (θ a b : ℝ) : ℝ

The cone function max 0 (1 - ‖(a, b)‖_θ).

Equations

• ProbabilityTheory.Copula.SpearmanNelsen2.cone θ a b = max 0 (1 - (|a| ^ θ + |b| ^ θ) ^ θ⁻¹)

theorem ProbabilityTheory.Copula.SpearmanNelsen2.continuous_cone (θ : ℝ) (hθ : 1 ≤ θ) : Continuous fun (z : Fin 2 → ℝ) => cone θ (z 0) (z 1)

theorem ProbabilityTheory.Copula.SpearmanNelsen2.cone_eq_zero (θ : ℝ) (hθ : 1 ≤ θ) {a b : ℝ} (h : 1 ≤ |a| ∨ 1 ≤ |b|) : cone θ a b = 0

theorem ProbabilityTheory.Copula.SpearmanNelsen2.cone_nonneg (θ a b : ℝ) : 0 ≤ cone θ a b

theorem ProbabilityTheory.Copula.SpearmanNelsen2.integrable_cone (θ : ℝ) (hθ : 1 ≤ θ) : MeasureTheory.Integrable (fun (z : Fin 2 → ℝ) => cone θ (z 0) (z 1)) MeasureTheory.volume

theorem ProbabilityTheory.Copula.SpearmanNelsen2.measure_lt_cone (θ : ℝ) (hθ : 1 ≤ θ) {t : ℝ} (ht : 0 < t) : MeasureTheory.volume {z : Fin 2 → ℝ | t < cone θ (z 0) (z 1)} = ENNReal.ofReal (1 - t) ^ 2 * ENNReal.ofReal ((2 * Real.Gamma (θ⁻¹ + 1)) ^ 2 / Real.Gamma (2 / θ + 1))

The volume of the level sets of the cone function.

theorem ProbabilityTheory.Copula.SpearmanNelsen2.integral_Ioi_max_sq : ∫ (t : ℝ) in Set.Ioi 0, max (1 - t) 0 ^ 2 = 1 / 3

theorem ProbabilityTheory.Copula.SpearmanNelsen2.integral_cone (θ : ℝ) (hθ : 1 ≤ θ) : ∫ (z : Fin 2 → ℝ), cone θ (z 0) (z 1) = (2 * Real.Gamma (θ⁻¹ + 1)) ^ 2 / Real.Gamma (2 / θ + 1) / 3

The integral of the cone function over the plane.

theorem ProbabilityTheory.Copula.SpearmanNelsen2.cone_abs_left (θ a b : ℝ) : cone θ |a| b = cone θ a b

theorem ProbabilityTheory.Copula.SpearmanNelsen2.cone_abs_right (θ a b : ℝ) : cone θ a |b| = cone θ a b

theorem ProbabilityTheory.Copula.SpearmanNelsen2.integral_cone_eq_quadrant (θ : ℝ) (hθ : 1 ≤ θ) : ∫ (z : Fin 2 → ℝ), cone θ (z 0) (z 1) = 4 * ∫ (x : ℝ) (y : ℝ) in Set.Ioi 0, cone θ x y

Reduction of the plane integral of the cone function to the positive quadrant.

theorem ProbabilityTheory.Copula.SpearmanNelsen2.integral_unit_one_sub (g : ℝ → ℝ) (hg : ∀ (t : ℝ), 1 ≤ t → g t = 0) : ∫ (t : ↑unitInterval), g (1 - ↑t) = ∫ (t : ℝ) in Set.Ioi 0, g t

Reflection of the unit interval and extension by zero to the positive half-line.

theorem ProbabilityTheory.Copula.SpearmanNelsen2.cone_comm (θ a b : ℝ) : cone θ a b = cone θ b a

theorem ProbabilityTheory.Copula.SpearmanNelsen2.cdf_nelsen2_eq_cone (θ : ℝ) (hθ : 1 ≤ θ) (u v : ↑unitInterval) : (nelsen2 θ hθ).cdf ![u, v] = cone θ (1 - ↑u) (1 - ↑v)

theorem ProbabilityTheory.Copula.spearmanRho_nelsen2 (θ : ℝ) (hθ : 1 ≤ θ) : (nelsen2 θ hθ).spearmanRho = 4 * Real.Gamma (θ⁻¹ + 1) ^ 2 / Real.Gamma (2 / θ + 1) - 3

Spearman's rho of Nelsen's family 2 (θ ≥ 1): ρ = 4 Γ(1 + 1/θ)² / Γ(1 + 2/θ) - 3.