← Copula mathematical handbook

Kendall distribution functions of Archimedean copulas

Restatement of Nelsen, An Introduction to Copulas, second edition, Theorem 4.3.4 for the library's Kendall distribution function Copula.kendallCDF (K_C(t) = P(C(U) ≤ t)): for a generator with continuously differentiable inverse generator, K_C(t) = t − φ(t) ψ'(φ(t)) = t − φ(t)/φ'(t) on (0, 1] (BivariateGenerator.IsC1.kendallCDF_eq, BivariateGenerator.IsC1.kendallCDF_eq_deriv).

At zero:

• K_C(0) = 0 for every strict generator (BivariateGenerator.IsStrict.kendallCDF_zero): the zero set of C is the boundary {u = 0} ∪ {v = 0}, a null set;
• Nelsen, Theorem 4.3.3: the mass of the zero set {C = 0} is K_C(0) = −lim_{t → 0+} φ(t)/φ'(t) = −φ(0)/φ'(0⁺) (BivariateGenerator.IsC1.kendallCDF_zero, BivariateGenerator.IsC1.measureReal_cdf_eq_zero), by right continuity of K_C;
• instances: W puts all its mass on the zero set (kendallCDF_zero_countermonotonic), and Nelsen's family 4.2.2 puts mass 1/θ there (kendallCDF_zero_nelsen2).

theorem ProbabilityTheory.Copula.BivariateGenerator.IsC1.kendallCDF_eq {g : BivariateGenerator} {ψ' : ℝ → ℝ} (h : g.IsC1 ψ') {t : ↑unitInterval} (ht : t ≠ 0) : g.copula.kendallCDF ↑t = ↑t - g.invFun t * ψ' (g.invFun t)

Nelsen, Theorem 4.3.4, for Copula.kendallCDF.

theorem ProbabilityTheory.Copula.BivariateGenerator.IsC1.kendallCDF_eq_deriv {g : BivariateGenerator} {ψ' : ℝ → ℝ} (h : g.IsC1 ψ') {t : ↑unitInterval} (ht : t ≠ 0) (ht1 : t ≠ 1) : g.copula.kendallCDF ↑t = ↑t - g.invFun t / deriv g.invFunReal ↑t

Nelsen, Theorem 4.3.4 in the form K_C(t) = t − φ(t)/φ'(t), 0 < t < 1.

theorem ProbabilityTheory.Copula.BivariateGenerator.IsStrict.kendallCDF_zero {g : BivariateGenerator} (hg : g.IsStrict) : g.copula.kendallCDF 0 = 0

For a strict generator the Kendall distribution has no atom at zero.

theorem ProbabilityTheory.Copula.BivariateGenerator.IsC1.kendallCDF_zero {g : BivariateGenerator} {ψ' : ℝ → ℝ} (h : g.IsC1 ψ') {m : ℝ} (hm : Filter.Tendsto (fun (t : ℝ) => g.invFunReal t * ψ' (g.invFunReal t)) (nhdsWithin 0 (Set.Ioi 0)) (nhds m)) : g.copula.kendallCDF 0 = -m

Nelsen, Theorem 4.3.3: for a C¹ generator, K_C(0) = −lim_{t → 0+} φ(t) ψ'(φ(t)), i.e. −φ(0)/φ'(0⁺), whenever this limit exists.

theorem ProbabilityTheory.Copula.BivariateGenerator.IsC1.measureReal_cdf_eq_zero {g : BivariateGenerator} {ψ' : ℝ → ℝ} (h : g.IsC1 ψ') {m : ℝ} (hm : Filter.Tendsto (fun (t : ℝ) => g.invFunReal t * ψ' (g.invFunReal t)) (nhdsWithin 0 (Set.Ioi 0)) (nhds m)) : g.copula.toMeasure.real {x : Fin 2 → ↑unitInterval | g.copula.cdf x = 0} = -m

Nelsen, Theorem 4.3.3: the C-measure of the zero set {C = 0} is −lim_{t → 0+} φ(t) ψ'(φ(t)) = −φ(0)/φ'(0⁺).

theorem ProbabilityTheory.Copula.kendallCDF_zero_countermonotonic : countermonotonic.kendallCDF 0 = 1

The lower Fréchet bound W concentrates on its zero set: K_W(0) = 1.

theorem ProbabilityTheory.Copula.kendallCDF_zero_nelsen2 (θ : ℝ) (hθ : 1 ≤ θ) : (nelsen2 θ hθ).kendallCDF 0 = 1 / θ

Nelsen's family 4.2.2 puts mass 1/θ on its zero set.