← Copula mathematical handbook

Kendall's tau of further families of Nelsen's Table 4.1

Applications of Nelsen's Corollary 5.1.4, τ = 1 + 4 ∫₀¹ φ(t) / φ'(t) dt (BivariateGenerator.kendallTau_eq_of_hasDerivAt), to the families of Nelsen, An Introduction to Copulas, second edition, Table 4.1 whose Kendall integrand is elementary:

• family 4.2.1 (Clayton) on its negative range −1 ≤ θ < 0: τ = θ / (θ + 2) (kendallTau_claytonNegative), completing kendallTau_clayton for θ > 0;
• family 4.2.7, 0 < θ ≤ 1: τ = 2 − 2/θ − 2 (1 − θ)² log(1 − θ) / θ² (kendallTau_nelsen7; θ = 1 is independence, with 0 · log 0 = 0), and τ = −1 at θ = 0 (W);
• family 4.2.8, θ ≥ 1: τ = (θ − 4) / (3θ) (kendallTau_nelsen8);
• family 4.2.15 (Genest–Ghoudi), θ ≥ 1: τ = (2θ − 3) / (2θ − 1) (kendallTau_genestGhoudi);
• family 4.2.18, θ ≥ 2: τ = 1 − 4 / (3θ) (kendallTau_nelsen18).

The integrands are (t^{θ+1} − t)/θ (Clayton, θ < 0), (θt + 1 − θ) log(θt + 1 − θ) / θ (#7), −(1 − t)(1 + (θ − 1)t)/θ (#8), −(t^{1 − 1/θ} − t) (#15) and −(t − 1)²/θ (#18). All five generators except #1 with θ = −1 limits are non-strict; kendallTau_eq_of_hasDerivAt covers strict and non-strict generators alike.

theorem ProbabilityTheory.Copula.KendallTauTable.invFunReal_of_mem (g : BivariateGenerator) {t : ℝ} (ht : t ∈ Set.Ioo 0 1) : g.invFunReal t = g.invFun ⟨t, ⋯⟩

The real extension of a generator at an interior point is its value there.

Clayton, negative parameters

theorem ProbabilityTheory.Copula.kendallTau_claytonNegative (θ : ℝ) (hθ : -1 ≤ θ) (hn : θ < 0) : (claytonNegative θ hθ hn).kendallTau = θ / (θ + 2)

Nelsen, Table 4.1 / Section 5.1.1: Kendall's tau of the Clayton copula for −1 ≤ θ < 0 is θ / (θ + 2).

Family 4.2.8

theorem ProbabilityTheory.Copula.kendallTau_nelsen8 (θ : ℝ) (hθ : 1 ≤ θ) : (nelsen8 θ hθ).kendallTau = (θ - 4) / (3 * θ)

Nelsen, Table 4.1, family 8 (θ ≥ 1): τ = (θ − 4) / (3θ).

Family 4.2.18

theorem ProbabilityTheory.Copula.kendallTau_nelsen18 (θ : ℝ) (hθ : 2 ≤ θ) : (nelsen18 θ hθ).kendallTau = 1 - 4 / (3 * θ)

Nelsen, Table 4.1, family 18 (θ ≥ 2): τ = 1 − 4 / (3θ).

Family 4.2.7

theorem ProbabilityTheory.Copula.integral_mul_log_of_nonneg {a b : ℝ} (ha : 0 ≤ a) (hab : a ≤ b) : ∫ (y : ℝ) in a..b, y * Real.log y = b * (b * Real.log b) / 2 - b ^ 2 / 4 - (a * (a * Real.log a) / 2 - a ^ 2 / 4)

∫_a^b y log y dy = F(b) − F(a) with F(y) = y² log y / 2 − y² / 4, for 0 ≤ a ≤ b.

theorem ProbabilityTheory.Copula.kendallTau_nelsen7 (θ : ↑unitInterval) (hθ : θ ≠ 0) : (nelsen7 θ).kendallTau = 2 - 2 / ↑θ - 2 * (1 - ↑θ) ^ 2 * Real.log (1 - ↑θ) / ↑θ ^ 2

Nelsen, Table 4.1, family 7 (0 < θ ≤ 1): τ = 2 − 2/θ − 2 (1 − θ)² log(1 − θ) / θ² (at θ = 1, independence, this is 0).

theorem ProbabilityTheory.Copula.kendallTau_nelsen7_zero : (nelsen7 0).kendallTau = -1

Family 7 at θ = 0 is W, with τ = −1.

Family 4.2.15 (Genest–Ghoudi)

theorem ProbabilityTheory.Copula.kendallTau_genestGhoudi (θ : ℝ) (hθ : 1 ≤ θ) : (genestGhoudi θ hθ).kendallTau = (2 * θ - 3) / (2 * θ - 1)

Nelsen, Table 4.1, family 15 (Genest–Ghoudi, θ ≥ 1): τ = (2θ − 3) / (2θ − 1).

Family 4.2.16

theorem ProbabilityTheory.Copula.kendallTau_nelsen16 (θ : ℝ) (hθ : 0 < θ) : (nelsen16 θ ⋯).kendallTau = 4 * θ - 1 - 4 * θ * Real.log ((1 + θ) / θ) + 4 * (1 - θ) * √θ * Real.arctan (1 / √θ)

Nelsen, Table 4.1, family 16 (θ > 0): τ = 4θ − 1 − 4θ log((1 + θ)/θ) + 4 (1 − θ) √θ arctan(1/√θ) (at θ = 0 the family is W with τ = −1).