← Copula mathematical handbook

The Galambos (negative logistic) extreme-value copula

For θ > 0 the Galambos Pickands function is

A(t) = 1 - (t^{-θ} + (1-t)^{-θ})^{-1/θ} = 1 - t (1 - t) / (t^θ + (1-t)^θ)^{1/θ}

(the second form is used as the definition, galambosPickands, since it is also correct at the endpoints). It is a Pickands function (isPickandsFunction_galambosPickands): the bounds follow from (t^θ + (1-t)^θ)^{1/θ} ≥ max(t, 1-t), and convexity of A from the superadditivity of the negative-order power mean (x^{-θ} + y^{-θ})^{-1/θ} (reverse Minkowski inequality, proved from the convexity of s ↦ s^{-θ}). The resulting copula galambos θ hθ has the classical CDF

C(u,v) = u v exp(((-log u)^{-θ} + (-log v)^{-θ})^{-1/θ}) (cdf_galambos),

and upper tail dependence coefficient λ_U = 2^{-1/θ} (hasUpperTailDependence_galambos).

References: J. Galambos, Order statistics of samples from multivariate distributions (1975); H. Joe, Dependence Modeling with Copulas (2014); G. Gudendorf and J. Segers, Extreme-value copulas (2010).

theorem ProbabilityTheory.Copula.convexOn_Icc_of_convexOn_Ioo {f : ℝ → ℝ} {a b : ℝ} (hc : ContinuousOn f (Set.Icc a b)) (h : ConvexOn ℝ (Set.Ioo a b) f) : ConvexOn ℝ (Set.Icc a b) f

A continuous function on [a,b] that is convex on (a,b) is convex on [a,b].

noncomputable def ProbabilityTheory.Copula.Galambos.negMean (θ x y : ℝ) : ℝ

The negative-order power mean (x^{-θ} + y^{-θ})^{-1/θ}.

Equations

• ProbabilityTheory.Copula.Galambos.negMean θ x y = (x ^ (-θ) + y ^ (-θ)) ^ (-θ⁻¹)

theorem ProbabilityTheory.Copula.Galambos.negMean_pos {θ x y : ℝ} (hx : 0 < x) (hy : 0 < y) : 0 < negMean θ x y

theorem ProbabilityTheory.Copula.Galambos.negMean_rpow {θ x y : ℝ} (hθ : 0 < θ) (hx : 0 < x) (hy : 0 < y) : negMean θ x y ^ (-θ) = x ^ (-θ) + y ^ (-θ)

theorem ProbabilityTheory.Copula.Galambos.negMean_superadditive {θ : ℝ} (hθ : 0 < θ) {x1 y1 x2 y2 : ℝ} (hx1 : 0 < x1) (hy1 : 0 < y1) (hx2 : 0 < x2) (hy2 : 0 < y2) : negMean θ x1 y1 + negMean θ x2 y2 ≤ negMean θ (x1 + x2) (y1 + y2)

Reverse Minkowski: the negative-order power mean is superadditive.

theorem ProbabilityTheory.Copula.Galambos.negMean_eq {θ x y : ℝ} (hθ : 0 < θ) (hx : 0 < x) (hy : 0 < y) : negMean θ x y = x * y / (x ^ θ + y ^ θ) ^ θ⁻¹

theorem ProbabilityTheory.Copula.Galambos.negMean_smul {θ c x y : ℝ} (hθ : 0 < θ) (hc : 0 < c) (hx : 0 < x) (hy : 0 < y) : negMean θ (c * x) (c * y) = c * negMean θ x y

noncomputable def ProbabilityTheory.Copula.galambosPickands (θ t : ℝ) : ℝ

The Galambos (negative logistic) Pickands function 1 - t (1-t) / (t^θ + (1-t)^θ)^{1/θ}.

Equations

• ProbabilityTheory.Copula.galambosPickands θ t = 1 - t * (1 - t) / (t ^ θ + (1 - t) ^ θ) ^ θ⁻¹

theorem ProbabilityTheory.Copula.galambosPickands_eq {θ t : ℝ} (hθ : 0 < θ) (ht : t ∈ Set.Ioo 0 1) : galambosPickands θ t = 1 - Galambos.negMean θ t (1 - t)

theorem ProbabilityTheory.Copula.isPickandsFunction_galambosPickands {θ : ℝ} (hθ : 0 < θ) : IsPickandsFunction (galambosPickands θ)

The Galambos function is a Pickands dependence function for every θ > 0.

noncomputable def ProbabilityTheory.Copula.galambos (θ : ℝ) (hθ : 0 < θ) : Copula 2

The Galambos copula, θ > 0.

Equations

• ProbabilityTheory.Copula.galambos θ hθ = ProbabilityTheory.Copula.pickandsCopula (ProbabilityTheory.Copula.galambosPickands θ) ⋯

theorem ProbabilityTheory.Copula.isExtremeValue_galambos {θ : ℝ} (hθ : 0 < θ) : (galambos θ hθ).IsExtremeValue

theorem ProbabilityTheory.Copula.cdf_galambos {θ : ℝ} (hθ : 0 < θ) {u v : ↑unitInterval} (hu : ↑u ∈ Set.Ioo 0 1) (hv : ↑v ∈ Set.Ioo 0 1) : (galambos θ hθ).cdf ![u, v] = ↑u * ↑v * Real.exp (((-Real.log ↑u) ^ (-θ) + (-Real.log ↑v) ^ (-θ)) ^ (-θ⁻¹))

The classical Galambos CDF u v exp(((-log u)^{-θ} + (-log v)^{-θ})^{-1/θ}) on (0,1)².

theorem ProbabilityTheory.Copula.hasUpperTailDependence_galambos {θ : ℝ} (hθ : 0 < θ) : (galambos θ hθ).HasUpperTailDependence (2 ^ (-θ⁻¹))

Upper tail dependence of the Galambos copula: λ_U = 2^{-1/θ}.