← Copula mathematical handbook

The Debye function of order two

D₂(θ) = (2/θ²) ∫₀^θ t² / (e^t − 1) dt (Nelsen, An Introduction to Copulas, second edition, Example 5.8; Genest 1987). Together with the Debye function of order one (debyeOne) it gives Spearman's rho of Frank's copula, ρ = 1 − (12/θ)(D₁(θ) − D₂(θ)) (Copula.Archimedean.SpearmanRhoFrank).

Basic properties: integrability of the integrand (intervalIntegrable_debyeTwo_integrand), non-negativity for θ ≥ 0 (debyeTwo_nonneg) and the reflection identity D₂(−x) = D₂(x) + 2x/3 (debyeTwo_neg).

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

The Debye function of order two, D₂(θ) = (2/θ²) ∫₀^θ t² / (e^t − 1) dt.

Equations

• ProbabilityTheory.Copula.debyeTwo θ = 2 / θ ^ 2 * ∫ (t : ℝ) in 0..θ, t ^ 2 / (Real.exp t - 1)

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

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

theorem ProbabilityTheory.Copula.debyeTwo_nonneg {θ : ℝ} (hθ : 0 ≤ θ) : 0 ≤ debyeTwo θ

D₂(θ) ≥ 0 for θ ≥ 0.

theorem ProbabilityTheory.Copula.debyeTwo_neg {x : ℝ} (hx : 0 < x) : debyeTwo (-x) = debyeTwo x + 2 * x / 3

Reflection identity of the second Debye function: D₂(−x) = D₂(x) + 2x/3.