← Copula mathematical handbook

The Kendall distribution function of an Archimedean copula

Nelsen, An Introduction to Copulas, second edition, Theorem 4.3.4: for an Archimedean copula with generator φ, the distribution function of C(U, V), where (U, V) has law C, is K_C(t) = P(C(U, V) ≤ t) = t − φ(t) / φ'(t⁺), 0 < t ≤ 1.

We prove this for generators whose inverse generator ψ = φ⁻¹ has a continuous derivative ψ' where it is positive (BivariateGenerator.IsC1), strict or not. Since φ'(t) = 1 / ψ'(φ(t)), the formula reads K_C(t) = t − φ(t) ψ'(φ(t)) (BivariateGenerator.IsC1.measureReal_cdf_le), and in Nelsen's form with the derivative of the generator (BivariateGenerator.IsC1.measureReal_cdf_le_deriv).

The proof disintegrates the copula measure along the first coordinate: for u > t the event C(u, V) ≤ t is V ≤ L_t(u) with the level curve L_t(u) = ψ(φ(t) − φ(u)), whose conditional probability is ∂₁C(u, L_t(u)) = ψ'(φ(t)) / ψ'(φ(u)) = φ'(u) / φ'(t); for u ≤ t it is one. Integrating gives t + (φ(1) − φ(t)) / φ'(t).

For a non-strict generator K_C has an atom at 0, the mass of the zero curve φ(u) + φ(v) = φ(0); its value −φ(0) / φ'(0⁺) (Nelsen, Theorem 4.3.3) is derived from the formula above in Copula.Archimedean.KendallCDF.

theorem ProbabilityTheory.Copula.measure_pair_preimage_eq_lintegral (C : Copula 2) {s : Set (↑unitInterval × ↑unitInterval)} (hs : MeasurableSet s) : C.toMeasure ((fun (x : Fin 2 → ↑unitInterval) => (x 0, x 1)) ⁻¹' s) = ∫⁻ (u : ↑unitInterval), (C.conditionalKernel u) (Prod.mk u ⁻¹' s)

Disintegration of a bivariate copula measure along the first coordinate.

theorem ProbabilityTheory.Copula.BivariateGenerator.toFun_le_iff (g : BivariateGenerator) {t : ↑unitInterval} (ht : t ≠ 0) {s : ℝ} (hs : 0 ≤ s) : g.toFun s ≤ ↑t ↔ g.invFun t ≤ s

ψ(s) ≤ t iff φ(t) ≤ s, for t > 0 and s ≥ 0.

theorem ProbabilityTheory.Copula.BivariateGenerator.cdf_le_iff_le_toI (g : BivariateGenerator) {t u : ↑unitInterval} (ht : t ≠ 0) (htu : t < u) (v : ↑unitInterval) : g.cdf u v ≤ ↑t ↔ v ≤ g.toI ⋯

The sections of {C ≤ t} beyond t are lower intervals bounded by the level curve.

theorem ProbabilityTheory.Copula.BivariateGenerator.IsC1.measureReal_cdf_le {g : BivariateGenerator} {ψ' : ℝ → ℝ} (h : g.IsC1 ψ') {t : ↑unitInterval} (ht : t ≠ 0) : g.copula.toMeasure.real {x : Fin 2 → ↑unitInterval | g.copula.cdf x ≤ ↑t} = ↑t - g.invFun t * ψ' (g.invFun t)

Nelsen, Theorem 4.3.4: the Kendall distribution function of the copula of a C¹ generator is K_C(t) = P(C(U, V) ≤ t) = t − φ(t) ψ'(φ(t)) for 0 < t ≤ 1.

theorem ProbabilityTheory.Copula.BivariateGenerator.IsC1.measureReal_cdf_le_deriv {g : BivariateGenerator} {ψ' : ℝ → ℝ} (h : g.IsC1 ψ') {t : ↑unitInterval} (ht : t ≠ 0) (ht1 : t ≠ 1) : g.copula.toMeasure.real {x : Fin 2 → ↑unitInterval | g.copula.cdf x ≤ ↑t} = ↑t - g.invFun t / deriv g.invFunReal ↑t

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