← Copula mathematical handbook

Kendall's tau from a differentiable generator

Nelsen, An Introduction to Copulas, second edition, Corollary 5.1.4 states τ_C = 1 + 4 ∫₀¹ φ(t) / φ'(t) dt in terms of the generator φ. The library's BivariateGenerator.IsC1.kendallTau_eq requires a continuous derivative of the inverse generator ψ. This file derives that hypothesis from the generator itself:

• BivariateGenerator.continuousAt_toFun: ψ is continuous on (0, ∞) (it is convex);
• BivariateGenerator.IsC1.of_invFunReal: if φ has a continuous nonvanishing derivative φ' on (0, 1), then ψ is C¹ on its positivity region with ψ'(s) = 1 / φ'(ψ(s)) (inverse function rule);
• BivariateGenerator.kendallTau_eq_of_hasDerivAt: then τ = 1 + 4 ∫₀¹ φ(t) / φ'(t) dt, for any explicit real function φ agreeing with the generator on (0, 1).

This is the form used for the families of Nelsen's Table 4.1 in Copula.Archimedean.KendallTauTable.

theorem ProbabilityTheory.Copula.BivariateGenerator.continuousAt_toFun (g : BivariateGenerator) {s : ℝ} (hs : 0 < s) : ContinuousAt g.toFun s

The inverse generator is continuous on (0, ∞), being convex on [0, ∞).

theorem ProbabilityTheory.Copula.BivariateGenerator.invFunReal_toFun (g : BivariateGenerator) {s : ℝ} (hs : 0 ≤ s) (hpos : 0 < g.toFun s) : g.invFunReal (g.toFun s) = s

φ(ψ(s)) = s for the real extension of the generator, where ψ(s) > 0.

theorem ProbabilityTheory.Copula.BivariateGenerator.IsC1.of_invFunReal {g : BivariateGenerator} {φ' : ℝ → ℝ} (hd : ∀ t ∈ Set.Ioo 0 1, HasDerivAt g.invFunReal (φ' t) t) (hc : ContinuousOn φ' (Set.Ioo 0 1)) (hne : ∀ t ∈ Set.Ioo 0 1, φ' t ≠ 0) : g.IsC1 fun (s : ℝ) => (φ' (g.toFun s))⁻¹

Inverse function rule: if the generator has a continuous nonvanishing derivative φ' on (0, 1), then the inverse generator is C¹ on its positivity region, with ψ'(s) = 1 / φ'(ψ(s)).

theorem ProbabilityTheory.Copula.BivariateGenerator.kendallTau_eq_of_invFunReal {g : BivariateGenerator} {φ' : ℝ → ℝ} (hd : ∀ t ∈ Set.Ioo 0 1, HasDerivAt g.invFunReal (φ' t) t) (hc : ContinuousOn φ' (Set.Ioo 0 1)) (hne : ∀ t ∈ Set.Ioo 0 1, φ' t ≠ 0) : g.copula.kendallTau = 1 + 4 * ∫ (t : ℝ) in 0..1, g.invFunReal t / φ' t

Nelsen, Corollary 5.1.4 in terms of the generator: if φ has a continuous nonvanishing derivative φ' on (0, 1), then τ = 1 + 4 ∫₀¹ φ(t) / φ'(t) dt.

theorem ProbabilityTheory.Copula.BivariateGenerator.kendallTau_eq_of_hasDerivAt {g : BivariateGenerator} {φ φ' : ℝ → ℝ} (heq : ∀ t ∈ Set.Ioo 0 1, g.invFunReal t = φ t) (hd : ∀ t ∈ Set.Ioo 0 1, HasDerivAt φ (φ' t) t) (hc : ContinuousOn φ' (Set.Ioo 0 1)) (hne : ∀ t ∈ Set.Ioo 0 1, φ' t ≠ 0) : g.copula.kendallTau = 1 + 4 * ∫ (t : ℝ) in 0..1, φ t / φ' t

Nelsen, Corollary 5.1.4 for an explicit generator: if φ agrees with the generator on (0, 1) and has a continuous nonvanishing derivative φ' there, then τ = 1 + 4 ∫₀¹ φ(t) / φ'(t) dt.