← Copula mathematical handbook

Kendall's tau of the Frank family as an elementary integral

For Frank's family (Nelsen, An Introduction to Copulas, second edition, family 4.2.5) with θ > 0, Nelsen's Corollary 5.1.4 gives τ = 1 + (4/θ) ∫₀¹ (e^{θt} − 1) log((1 − e^{−θt}) / (1 − e^{−θ})) dt (kendallTau_frank). Nelsen writes this through the Debye function as τ = 1 − (4/θ)(1 − D₁(θ)); the passage to the Debye form (an integration by parts and a substitution) is not formalized here.

The inverse generator ψ(s) = −log(1 − (1 − e^{−θ}) e^{−s}) / θ is strict and smooth (isC1_frankGenerator).

noncomputable def ProbabilityTheory.Copula.frankGeneratorDeriv (θ s : ℝ) : ℝ

The derivative of Frank's inverse generator.

Equations

• ProbabilityTheory.Copula.frankGeneratorDeriv θ s = -((1 - Real.exp (-θ)) * Real.exp (-s)) / (θ * (1 - (1 - Real.exp (-θ)) * Real.exp (-s)))

theorem ProbabilityTheory.Copula.isC1_frankGenerator (θ : ℝ) (hθ : 0 < θ) : (frankGenerator θ hθ).IsC1 (frankGeneratorDeriv θ)

Frank's inverse generator is continuously differentiable on (0, ∞).

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

Nelsen, Corollary 5.1.4 for Frank's family: τ = 1 + (4/θ) ∫₀¹ (e^{θt} − 1) log((1 − e^{−θt}) / (1 − e^{−θ})) dt.