← Copula mathematical handbook

Kendall's tau of Table 4.1 families as explicit integrals

For several families of Nelsen, An Introduction to Copulas, second edition, Table 4.1, the Kendall integral τ = 1 + 4 ∫₀¹ φ(t) / φ'(t) dt (Corollary 5.1.4, BivariateGenerator.kendallTau_eq_of_hasDerivAt) is not elementary (it involves exponential integrals, incomplete gamma functions or digamma values). This file records the explicit integral form for each of them:

• family 4.2.6 (Joe), θ ≥ 1: τ = 1 + (4/θ) ∫₀¹ (1 − (1−t)^θ) log(1 − (1−t)^θ) / (1−t)^{θ−1} dt (kendallTau_joe);
• family 4.2.9, 0 < θ ≤ 1: τ = 1 − (4/θ) ∫₀¹ t (1 − θ log t) log(1 − θ log t) dt (kendallTau_nelsen9);
• family 4.2.13, θ > 0: τ = 1 − (4/θ) ∫₀¹ t ((1 − log t) − (1 − log t)^{1−θ}) dt (kendallTau_nelsen13);
• family 4.2.19, θ > 0: τ = 1 − (4/θ) ∫₀¹ t² (1 − e^{θ − θ/t}) dt (kendallTau_nelsen19);
• family 4.2.20, θ > 0: τ = 1 − (4/θ) ∫₀¹ t^{θ+1} (1 − e^{1 − t^{−θ}}) dt (kendallTau_nelsen20).

theorem ProbabilityTheory.Copula.KendallTauIntegral.integral_congr_Ioo {f g : ℝ → ℝ} (h : ∀ t ∈ Set.Ioo 0 1, f t = g t) : ∫ (t : ℝ) in 0..1, f t = ∫ (t : ℝ) in 0..1, g t

Two integrands that agree on (0, 1) have the same integral over [0, 1].

theorem ProbabilityTheory.Copula.KendallTauIntegral.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.

theorem ProbabilityTheory.Copula.KendallTauIntegral.log_neg {t : ℝ} (ht : t ∈ Set.Ioo 0 1) : Real.log t < 0

theorem ProbabilityTheory.Copula.kendallTau_nelsen9 (θ : ℝ) (hθ : 0 < θ) (h1 : θ ≤ 1) : (nelsen9 θ hθ h1).kendallTau = 1 - 4 / θ * ∫ (t : ℝ) in 0..1, t * (1 - θ * Real.log t) * Real.log (1 - θ * Real.log t)

Nelsen, Table 4.1, family 9 (0 < θ ≤ 1): τ = 1 − (4/θ) ∫₀¹ t (1 − θ log t) log(1 − θ log t) dt.

theorem ProbabilityTheory.Copula.kendallTau_nelsen13 (θ : ℝ) (hθ : 0 < θ) : (nelsen13 θ hθ).kendallTau = 1 - 4 / θ * ∫ (t : ℝ) in 0..1, t * (1 - Real.log t - (1 - Real.log t) ^ (1 - θ))

Nelsen, Table 4.1, family 13 (θ > 0): τ = 1 − (4/θ) ∫₀¹ t ((1 − log t) − (1 − log t)^{1−θ}) dt (at θ = 1, independence, the integrand is −t log t and τ = 0).

theorem ProbabilityTheory.Copula.kendallTau_nelsen19 (θ : ℝ) (hθ : 0 < θ) : (nelsen19 θ hθ).kendallTau = 1 - 4 / θ * ∫ (t : ℝ) in 0..1, t ^ 2 * (1 - Real.exp (θ - θ / t))

Nelsen, Table 4.1, family 19 (θ > 0): τ = 1 − (4/θ) ∫₀¹ t² (1 − e^{θ − θ/t}) dt.

theorem ProbabilityTheory.Copula.kendallTau_nelsen20 (θ : ℝ) (hθ : 0 < θ) : (nelsen20 θ hθ).kendallTau = 1 - 4 / θ * ∫ (t : ℝ) in 0..1, t ^ (θ + 1) * (1 - Real.exp (1 - t ^ (-θ)))

Nelsen, Table 4.1, family 20 (θ > 0): τ = 1 − (4/θ) ∫₀¹ t^{θ+1} (1 − e^{1 − t^{−θ}}) dt.

theorem ProbabilityTheory.Copula.kendallTau_joe (θ : ℝ) (hθ : 1 ≤ θ) : (joe θ hθ).kendallTau = 1 + 4 / θ * ∫ (t : ℝ) in 0..1, (1 - (1 - t) ^ θ) * Real.log (1 - (1 - t) ^ θ) / (1 - t) ^ (θ - 1)

Nelsen, Table 4.1, family 6 (Joe, θ ≥ 1): τ = 1 + (4/θ) ∫₀¹ (1 − (1−t)^θ) log(1 − (1−t)^θ) / (1−t)^{θ−1} dt.