← Copula mathematical handbook

Kendall's tau of the Frank family in Debye form

Nelsen, An Introduction to Copulas, second edition, Example 5.4 / Table 4.1 (family 4.2.5): for Frank's family with parameter θ > 0, τ_θ = 1 − (4/θ) (1 − D₁(θ)), where D₁(θ) = (1/θ) ∫₀^θ t / (e^t − 1) dt is the Debye function of order one (debyeOne).

kendallTau_frank (Corollary 5.1.4) gives τ = 1 + (4/θ) ∫₀¹ (e^{θt} − 1) log((1 − e^{−θt}) / (1 − e^{−θ})) dt. After the substitution x = θ t, an integration by parts against F(x) = e^x − 1 − x (with the boundary term at 0 vanishing because F(x) ≤ x (e^x − 1) and |w log w| ≤ 1) turns this into ∫₀^θ (e^x − 1) log(...) dx = −θ + ∫₀^θ x / (e^x − 1) dx (frank_integral_eq_debye), which is the Debye form (kendallTau_frank_debye).

For θ < 0 (frankNegative θ, the reflection of Frank's copula with parameter −θ), the same formula holds (kendallTau_frankNegative_debye), by τ(C^{σ₂}) = −τ(C) and the reflection identity D₁(−x) = D₁(x) + x/2 (debyeOne_neg).

noncomputable def ProbabilityTheory.Copula.debyeOne (θ : ℝ) : ℝ

The Debye function of order one, D₁(θ) = (1/θ) ∫₀^θ t / (e^t − 1) dt.

Equations

• ProbabilityTheory.Copula.debyeOne θ = θ⁻¹ * ∫ (t : ℝ) in 0..θ, t / (Real.exp t - 1)

theorem ProbabilityTheory.Copula.FrankDebye.frank_integral_eq_debye {θ : ℝ} (hθ : 0 < θ) : ∫ (x : ℝ) in 0..θ, (Real.exp x - 1) * Real.log ((1 - Real.exp (-x)) / (1 - Real.exp (-θ))) = -θ + ∫ (x : ℝ) in 0..θ, x / (Real.exp x - 1)

The key identity: ∫₀^θ (e^x − 1) log((1 − e^{−x}) / (1 − e^{−θ})) dx = −θ + ∫₀^θ x/(e^x − 1) dx.

theorem ProbabilityTheory.Copula.kendallTau_frank_debye (θ : ℝ) (hθ : 0 < θ) : (frank θ hθ).kendallTau = 1 - 4 / θ * (1 - debyeOne θ)

Nelsen, Example 5.4 / Table 4.1 (family 4.2.5): Kendall's tau of Frank's copula in Debye form, τ_θ = 1 − (4/θ) (1 − D₁(θ)) for θ > 0.

theorem ProbabilityTheory.Copula.intervalIntegrable_debye_integrand {x : ℝ} (hx : 0 < x) : IntervalIntegrable (fun (t : ℝ) => t / (Real.exp t - 1)) MeasureTheory.volume 0 x

The integrand t/(e^t − 1) of the Debye function is interval integrable on [0, x].

theorem ProbabilityTheory.Copula.debyeOne_neg {x : ℝ} (hx : 0 < x) : debyeOne (-x) = debyeOne x + x / 2

Reflection identity of the Debye function: D₁(−x) = D₁(x) + x/2 for x > 0.

theorem ProbabilityTheory.Copula.kendallTau_frankNegative_debye (θ : ℝ) (hθ : θ < 0) : (frankNegative θ hθ).kendallTau = 1 - 4 / θ * (1 - debyeOne θ)

Nelsen, Example 5.4 / Table 4.1 (family 4.2.5) for negative parameters: Kendall's tau of Frank's copula frankNegative θ (θ < 0) is 1 − (4/θ) (1 − D₁(θ)).