← Copula mathematical handbook

Kendall's tau of families 10, 11 and 17 of Nelsen's Table 4.1

Explicit integral forms of τ = 1 + 4 ∫₀¹ φ(t) / φ'(t) dt (Nelsen, Corollary 5.1.4, BivariateGenerator.kendallTau_eq_of_hasDerivAt) for three families whose Kendall integral is not elementary:

• family 4.2.10, 0 < θ ≤ 1, φ(t) = log (2 t^{−θ} − 1): τ = 1 − (2/θ) ∫₀¹ t (2 − t^θ) log (2 t^{−θ} − 1) dt (kendallTau_nelsen10);
• family 4.2.11, 0 < θ ≤ 1/2, φ(t) = log (2 − t^θ): τ = 1 − (4/θ) ∫₀¹ t^{1−θ} (2 − t^θ) log (2 − t^θ) dt (kendallTau_nelsen11);
• family 4.2.17, θ ≠ 0, φ(t) = −log (((1+t)^{−θ} − 1) / (2^{−θ} − 1)): τ = 1 − (4/θ) ∫₀¹ (1+t) (1 − (1+t)^θ) log (((1+t)^{−θ} − 1) / (2^{−θ} − 1)) dt (kendallTau_nelsen17).

theorem ProbabilityTheory.Copula.kendallTau_nelsen10 (θ : ℝ) (hθ : 0 < θ) (h1 : θ ≤ 1) : (nelsen10 θ hθ h1).kendallTau = 1 - 2 / θ * ∫ (t : ℝ) in 0..1, t * (2 - t ^ θ) * Real.log (2 * t ^ (-θ) - 1)

Nelsen, Table 4.1, family 10 (0 < θ ≤ 1): τ = 1 − (2/θ) ∫₀¹ t (2 − t^θ) log (2 t^{−θ} − 1) dt.

theorem ProbabilityTheory.Copula.kendallTau_nelsen11 (θ : ℝ) (hθ : 0 < θ) (h2 : θ ≤ 1 / 2) : (nelsen11 θ hθ h2).kendallTau = 1 - 4 / θ * ∫ (t : ℝ) in 0..1, t ^ (1 - θ) * (2 - t ^ θ) * Real.log (2 - t ^ θ)

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

theorem ProbabilityTheory.Copula.kendallTau_nelsen17 (θ : ℝ) (hθ : θ ≠ 0) : (nelsen17 θ hθ).kendallTau = 1 - 4 / θ * ∫ (t : ℝ) in 0..1, (1 + t) * (1 - (1 + t) ^ θ) * Real.log (((1 + t) ^ (-θ) - 1) / (2 ^ (-θ) - 1))

Nelsen, Table 4.1, family 17 (θ ≠ 0): τ = 1 − (4/θ) ∫₀¹ (1+t) (1 − (1+t)^θ) log (((1+t)^{−θ} − 1) / (2^{−θ} − 1)) dt.