← Copula mathematical handbook

Kendall's tau of extreme-value copulas

For a Pickands dependence function A which is differentiable on (0,1),

τ(C_A) = 1 - ∫₀¹ (A(t) - t A'(t)) (A(t) + (1-t) A'(t)) / A(t)² dt (kendallTau_pickandsCopula),

and if moreover A is twice differentiable on (0,1) with integrable A'', integration by parts gives the classical formula

τ(C_A) = ∫₀¹ t (1-t) A''(t) / A(t) dt (kendallTau_pickandsCopula_of_deriv2),

i.e. τ = ∫₀¹ t(1-t)/A(t) dA'(t).

Proof. By kendallTau_conditional_product, τ = 1 - 4 ∬ ∂₁C ∂₂C. For C_A the partial derivatives are ∂₁C(u,v) = C(u,v) u⁻¹ (A(r) - r A'(r)) and ∂₂C(u,v) = C(u,v) v⁻¹ (A(r) + (1-r) A'(r)) with r = log v / log(uv); the conditional distribution functions agree with them almost everywhere (conditionalCDF_eq_deriv, and the transpose C_A^T = C_{A(1-·)}). The double integral is then computed with the same substitution u = v^{1/t - 1} and Gamma integral as Spearman's rho (Copula.ExtremeValue.PickandsSpearman).

References: G. Gudendorf and J. Segers, Extreme-value copulas (2010); C. Genest and L.-P. Rivest, A characterization of Gumbel's family of extreme value distributions (1989); H. Joe, Dependence Modeling with Copulas (2014).

theorem ProbabilityTheory.Copula.transpose_pickandsCopula {A : ℝ → ℝ} (hA : IsPickandsFunction A) : (pickandsCopula A hA).transpose = pickandsCopula (fun (t : ℝ) => A (1 - t)) ⋯

The transpose of C_A is the Pickands copula of t ↦ A(1 - t).

noncomputable def ProbabilityTheory.Copula.PickandsKendall.ratio (x y : ℝ) : ℝ

The ratio log y / log (x y), the Pickands coordinate of (x,y).

Equations

• ProbabilityTheory.Copula.PickandsKendall.ratio x y = Real.log y / Real.log (x * y)

theorem ProbabilityTheory.Copula.PickandsKendall.ratio_mem {x y : ℝ} (hx : x ∈ Set.Ioo 0 1) (hy : y ∈ Set.Ioo 0 1) : ratio x y ∈ Set.Ioo 0 1

noncomputable def ProbabilityTheory.Copula.PickandsKendall.d1 (A : ℝ → ℝ) (x y : ℝ) : ℝ

The partial derivative ∂₁ C_A(x,y) = C_A(x,y) x⁻¹ (A(r) - r A'(r)) on (0,1)², and 0 elsewhere.

Equations

• One or more equations did not get rendered due to their size.

theorem ProbabilityTheory.Copula.PickandsKendall.measurable_d1 {A : ℝ → ℝ} (hA : IsPickandsFunction A) : Measurable fun (p : ℝ × ℝ) => d1 A p.1 p.2

theorem ProbabilityTheory.Copula.PickandsKendall.deriv_bounds {A : ℝ → ℝ} (hA : IsPickandsFunction A) {t : ℝ} (ht : t ∈ Set.Ioo 0 1) (hd : DifferentiableAt ℝ A t) : 0 ≤ A t - t * deriv A t ∧ A t - t * deriv A t ≤ 1 ∧ 0 ≤ A t + (1 - t) * deriv A t ∧ A t + (1 - t) * deriv A t ≤ 1

Tangent-line bounds for a differentiable Pickands function: 0 ≤ A - tA' ≤ 1 and 0 ≤ A + (1-t)A' ≤ 1.

theorem ProbabilityTheory.Copula.PickandsKendall.d1_nonneg {A : ℝ → ℝ} (hA : IsPickandsFunction A) (hdiff : DifferentiableOn ℝ A (Set.Ioo 0 1)) (x y : ℝ) : 0 ≤ d1 A x y

theorem ProbabilityTheory.Copula.PickandsKendall.hasDerivAt_kernel {A : ℝ → ℝ} {u v : ℝ} (hu : u ∈ Set.Ioo 0 1) (hv : v ∈ Set.Ioo 0 1) (hd : DifferentiableAt ℝ A (ratio u v)) : HasDerivAt (fun (x : ℝ) => PickandsSpearman.kernel A x v) (PickandsSpearman.kernel A u v * (u⁻¹ * (PickandsSpearman.extend A (ratio u v) - ratio u v * deriv A (ratio u v)))) u

The derivative of the Pickands CDF in its first variable.

theorem ProbabilityTheory.Copula.PickandsKendall.deriv_cdfSection {A : ℝ → ℝ} (hA : IsPickandsFunction A) (hdiff : DifferentiableOn ℝ A (Set.Ioo 0 1)) {u : ℝ} (hu : u ∈ Set.Ioo 0 1) {v : ↑unitInterval} (hv : ↑v ∈ Set.Ioo 0 1) : deriv ((pickandsCopula A hA).cdfSection v) u = d1 A u ↑v

The CDF section of C_A has derivative ∂₁ C_A at interior points.

theorem ProbabilityTheory.Copula.PickandsKendall.ae_coe_mem_Ioo : ∀ᵐ (v : ↑unitInterval), ↑v ∈ Set.Ioo 0 1

theorem ProbabilityTheory.Copula.PickandsKendall.ae_conditionalCDF_eq {A : ℝ → ℝ} (hA : IsPickandsFunction A) (hdiff : DifferentiableOn ℝ A (Set.Ioo 0 1)) {w : ↑unitInterval} (hw : ↑w ∈ Set.Ioo 0 1) : ∀ᵐ (u : ↑unitInterval), (pickandsCopula A hA).conditionalCDF u w = d1 A ↑u ↑w

For each interior w, the conditional CDF of C_A is ∂₁ C_A(·, w) almost everywhere.

theorem ProbabilityTheory.Copula.PickandsKendall.differentiableOn_comp_one_sub {A : ℝ → ℝ} (hdiff : DifferentiableOn ℝ A (Set.Ioo 0 1)) : DifferentiableOn ℝ (fun (t : ℝ) => A (1 - t)) (Set.Ioo 0 1)

theorem ProbabilityTheory.Copula.PickandsKendall.ae_cross_eq {A : ℝ → ℝ} (hA : IsPickandsFunction A) (hdiff : DifferentiableOn ℝ A (Set.Ioo 0 1)) : ∀ᵐ (p : ↑unitInterval × ↑unitInterval), (pickandsCopula A hA).conditionalCDF p.1 p.2 * (pickandsCopula A hA).transpose.conditionalCDF p.2 p.1 = d1 A ↑p.1 ↑p.2 * d1 (fun (t : ℝ) => A (1 - t)) ↑p.2 ↑p.1

The integrand of Kendall's formula agrees a.e. with ∂₁C ∂₂C.

theorem ProbabilityTheory.Copula.PickandsKendall.substMap_mem {y t : ℝ} (hy : y ∈ Set.Ioo 0 1) (ht : t ∈ Set.Ioo 0 1) : PickandsSpearman.substMap y t ∈ Set.Ioo 0 1

theorem ProbabilityTheory.Copula.PickandsKendall.ratio_substMap_swap {y t : ℝ} (hy : y ∈ Set.Ioo 0 1) (ht : t ∈ Set.Ioo 0 1) : ratio y (PickandsSpearman.substMap y t) = 1 - t

noncomputable def ProbabilityTheory.Copula.PickandsKendall.cross (A : ℝ → ℝ) (x y : ℝ) : ℝ

The product ∂₁C_A(x,y) ∂₂C_A(x,y), written with the first partial derivative of the transposed copula.

Equations

• ProbabilityTheory.Copula.PickandsKendall.cross A x y = ProbabilityTheory.Copula.PickandsKendall.d1 A x y * ProbabilityTheory.Copula.PickandsKendall.d1 (fun (t : ℝ) => A (1 - t)) y x

noncomputable def ProbabilityTheory.Copula.PickandsKendall.pq (A : ℝ → ℝ) (t : ℝ) : ℝ

The numerator (A - tA')(A + (1-t)A').

Equations

• One or more equations did not get rendered due to their size.

noncomputable def ProbabilityTheory.Copula.PickandsKendall.kernelK (A : ℝ → ℝ) (t y : ℝ) : ℝ

The integrand of the Kendall computation after the substitution x = y^{1/t - 1}.

Equations

• One or more equations did not get rendered due to their size.

theorem ProbabilityTheory.Copula.PickandsKendall.measurable_pq {A : ℝ → ℝ} (hA : IsPickandsFunction A) : Measurable (pq A)

theorem ProbabilityTheory.Copula.PickandsKendall.measurable_kernelK {A : ℝ → ℝ} (hA : IsPickandsFunction A) : Measurable fun (p : ℝ × ℝ) => kernelK A p.2 p.1

theorem ProbabilityTheory.Copula.PickandsKendall.pq_bounds {A : ℝ → ℝ} (hA : IsPickandsFunction A) (hdiff : DifferentiableOn ℝ A (Set.Ioo 0 1)) {t : ℝ} (ht : t ∈ Set.Ioo 0 1) : 0 ≤ pq A t ∧ pq A t ≤ 1

theorem ProbabilityTheory.Copula.PickandsKendall.substJac_mul_cross {A : ℝ → ℝ} {y t : ℝ} (hy : y ∈ Set.Ioo 0 1) (ht : t ∈ Set.Ioo 0 1) : PickandsSpearman.substJac y t * cross A (PickandsSpearman.substMap y t) y = kernelK A t y

theorem ProbabilityTheory.Copula.PickandsKendall.integral_cross {A : ℝ → ℝ} (hA : IsPickandsFunction A) (hdiff : DifferentiableOn ℝ A (Set.Ioo 0 1)) : ∫ (p : ↑unitInterval × ↑unitInterval), cross A ↑p.1 ↑p.2 = ∫ (t : ℝ) in Set.Ioo 0 1, pq A t / (4 * PickandsSpearman.extend A t ^ 2)

The double integral ∬ ∂₁C_A ∂₂C_A = ∫₀¹ (A - tA')(A + (1-t)A') / (4A²) dt.

theorem ProbabilityTheory.Copula.kendallTau_pickandsCopula {A : ℝ → ℝ} (hA : IsPickandsFunction A) (hdiff : DifferentiableOn ℝ A (Set.Ioo 0 1)) : (pickandsCopula A hA).kendallTau = 1 - ∫ (t : ℝ) in 0..1, (A t - t * deriv A t) * (A t + (1 - t) * deriv A t) / A t ^ 2

Kendall's tau of a Pickands copula with A differentiable on (0,1): τ(C_A) = 1 - ∫₀¹ (A(t) - t A'(t)) (A(t) + (1-t) A'(t)) / A(t)² dt.

theorem ProbabilityTheory.Copula.IsPickandsFunction.continuousOn {A : ℝ → ℝ} (hA : IsPickandsFunction A) : ContinuousOn A (Set.Icc 0 1)

A Pickands function is continuous on [0,1].

theorem ProbabilityTheory.Copula.kendallTau_pickandsCopula_of_deriv2 {A A'' : ℝ → ℝ} (hA : IsPickandsFunction A) (hdiff : DifferentiableOn ℝ A (Set.Ioo 0 1)) (h2 : ∀ t ∈ Set.Ioo 0 1, HasDerivAt (deriv A) (A'' t) t) (hint : IntervalIntegrable A'' MeasureTheory.volume 0 1) : (pickandsCopula A hA).kendallTau = ∫ (t : ℝ) in 0..1, t * (1 - t) * A'' t / A t

Kendall's tau of a Pickands copula (twice differentiable A): τ(C_A) = ∫₀¹ t (1-t) A''(t) / A(t) dt, i.e. τ = ∫₀¹ t(1-t)/A(t) dA'(t).