← Copula mathematical handbook

The Hüsler–Reiss extreme-value copula

Let Φ be the standard normal distribution function (ProbabilityTheory.cdf (gaussianReal 0 1)) and λ > 0. With the logit z(t) = log t - log(1 - t), the Hüsler–Reiss Pickands function is

A(t) = (1 - t) Φ(λ - z(t)/(2λ)) + t Φ(λ + z(t)/(2λ)), 0 < t < 1,

with A(0) = A(1) = 1 (hueslerReissPickands). Because (1 - t) φ(λ - z/(2λ)) = t φ(λ + z/(2λ)), its derivative is A'(t) = Φ(λ + z(t)/(2λ)) - Φ(λ - z(t)/(2λ)), which is nondecreasing and lies in [-1, 1]; hence A is convex, continuous at the endpoints (limits of Φ at ±∞), and max(t, 1 - t) ≤ A(t) ≤ 1 (mean value theorem). So A is a Pickands function (isPickandsFunction_hueslerReissPickands) and defines the Hüsler–Reiss copula hueslerReiss, symmetric (A(1 - t) = A(t)), with A(1/2) = Φ(λ) and upper tail dependence coefficient λ_U = 2 (1 - Φ(λ)) (hasUpperTailDependence_hueslerReiss).

References: J. Hüsler and R.-D. Reiss, Maxima of normal random vectors: between independence and complete dependence (1989); G. Gudendorf and J. Segers, Extreme-value copulas (2010); H. Joe, Dependence Modeling with Copulas (2014).

noncomputable def ProbabilityTheory.Copula.HueslerReiss.stdNormalCDF (x : ℝ) : ℝ

The standard normal distribution function Φ.

Equations

• ProbabilityTheory.Copula.HueslerReiss.stdNormalCDF x = ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1)) x

noncomputable def ProbabilityTheory.Copula.HueslerReiss.stdNormalPDF (x : ℝ) : ℝ

The standard normal density φ.

Equations

• ProbabilityTheory.Copula.HueslerReiss.stdNormalPDF x = ProbabilityTheory.gaussianPDFReal 0 1 x

theorem ProbabilityTheory.Copula.HueslerReiss.stdNormalCDF_nonneg (x : ℝ) : 0 ≤ stdNormalCDF x

theorem ProbabilityTheory.Copula.HueslerReiss.stdNormalCDF_le_one (x : ℝ) : stdNormalCDF x ≤ 1

theorem ProbabilityTheory.Copula.HueslerReiss.monotone_stdNormalCDF : Monotone stdNormalCDF

theorem ProbabilityTheory.Copula.HueslerReiss.continuous_stdNormalPDF : Continuous stdNormalPDF

theorem ProbabilityTheory.Copula.HueslerReiss.hasDerivAt_stdNormalCDF (x : ℝ) : HasDerivAt stdNormalCDF (stdNormalPDF x) x

Φ' = φ.

noncomputable def ProbabilityTheory.Copula.HueslerReiss.logit (t : ℝ) : ℝ

The logit log t - log (1 - t).

Equations

• ProbabilityTheory.Copula.HueslerReiss.logit t = Real.log t - Real.log (1 - t)

theorem ProbabilityTheory.Copula.HueslerReiss.logit_one_sub (t : ℝ) : logit (1 - t) = -logit t

theorem ProbabilityTheory.Copula.HueslerReiss.hasDerivAt_logit {t : ℝ} (ht : t ∈ Set.Ioo 0 1) : HasDerivAt logit (t⁻¹ + (1 - t)⁻¹) t

theorem ProbabilityTheory.Copula.HueslerReiss.logit_mono {s t : ℝ} (hs : s ∈ Set.Ioo 0 1) (ht : t ∈ Set.Ioo 0 1) (hst : s ≤ t) : logit s ≤ logit t

theorem ProbabilityTheory.Copula.HueslerReiss.pdf_identity {lam t : ℝ} (hlam : 0 < lam) (ht : t ∈ Set.Ioo 0 1) : (1 - t) * stdNormalPDF (lam - logit t / (2 * lam)) = t * stdNormalPDF (lam + logit t / (2 * lam))

The Gaussian density identity behind the Hüsler–Reiss derivative.

noncomputable def ProbabilityTheory.Copula.HueslerReiss.hrInner (lam t : ℝ) : ℝ

The Hüsler–Reiss function on (0,1).

Equations

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

theorem ProbabilityTheory.Copula.HueslerReiss.inner_one_sub (lam t : ℝ) : hrInner lam (1 - t) = hrInner lam t

theorem ProbabilityTheory.Copula.HueslerReiss.hasDerivAt_inner {lam t : ℝ} (hlam : 0 < lam) (ht : t ∈ Set.Ioo 0 1) : HasDerivAt (hrInner lam) (stdNormalCDF (lam + logit t / (2 * lam)) - stdNormalCDF (lam - logit t / (2 * lam))) t

noncomputable def ProbabilityTheory.Copula.hueslerReissPickands (lam t : ℝ) : ℝ

The Hüsler–Reiss Pickands function (λ > 0).

Equations

• ProbabilityTheory.Copula.hueslerReissPickands lam t = if t ∈ Set.Ioo 0 1 then ProbabilityTheory.Copula.HueslerReiss.hrInner lam t else 1

theorem ProbabilityTheory.Copula.HueslerReiss.pickands_eq_inner {lam t : ℝ} (ht : t ∈ Set.Ioo 0 1) : hueslerReissPickands lam t = hrInner lam t

theorem ProbabilityTheory.Copula.HueslerReiss.pickands_one_sub (lam t : ℝ) : hueslerReissPickands lam (1 - t) = hueslerReissPickands lam t

theorem ProbabilityTheory.Copula.HueslerReiss.hasDerivAt_pickands {lam t : ℝ} (hlam : 0 < lam) (ht : t ∈ Set.Ioo 0 1) : HasDerivAt (hueslerReissPickands lam) (stdNormalCDF (lam + logit t / (2 * lam)) - stdNormalCDF (lam - logit t / (2 * lam))) t

theorem ProbabilityTheory.Copula.HueslerReiss.continuousWithinAt_zero {lam : ℝ} (hlam : 0 < lam) : ContinuousWithinAt (hueslerReissPickands lam) (Set.Icc 0 1) 0

theorem ProbabilityTheory.Copula.HueslerReiss.continuousOn_pickands {lam : ℝ} (hlam : 0 < lam) : ContinuousOn (hueslerReissPickands lam) (Set.Icc 0 1)

theorem ProbabilityTheory.Copula.HueslerReiss.deriv_pickands_mem {lam t : ℝ} (hlam : 0 < lam) (ht : t ∈ Set.Ioo 0 1) : -1 ≤ deriv (hueslerReissPickands lam) t ∧ deriv (hueslerReissPickands lam) t ≤ 1

theorem ProbabilityTheory.Copula.isPickandsFunction_hueslerReissPickands {lam : ℝ} (hlam : 0 < lam) : IsPickandsFunction (hueslerReissPickands lam)

The Hüsler–Reiss function is a Pickands dependence function for every λ > 0.

noncomputable def ProbabilityTheory.Copula.hueslerReiss (lam : ℝ) (hlam : 0 < lam) : Copula 2

The Hüsler–Reiss copula, λ > 0.

Equations

• ProbabilityTheory.Copula.hueslerReiss lam hlam = ProbabilityTheory.Copula.pickandsCopula (ProbabilityTheory.Copula.hueslerReissPickands lam) ⋯

theorem ProbabilityTheory.Copula.isExtremeValue_hueslerReiss {lam : ℝ} (hlam : 0 < lam) : (hueslerReiss lam hlam).IsExtremeValue

theorem ProbabilityTheory.Copula.hueslerReissPickands_half (lam : ℝ) : hueslerReissPickands lam (1 / 2) = HueslerReiss.stdNormalCDF lam

theorem ProbabilityTheory.Copula.hasUpperTailDependence_hueslerReiss {lam : ℝ} (hlam : 0 < lam) : (hueslerReiss lam hlam).HasUpperTailDependence (2 * (1 - HueslerReiss.stdNormalCDF lam))

Upper tail dependence of the Hüsler–Reiss copula: λ_U = 2 (1 - Φ(λ)).

theorem ProbabilityTheory.Copula.hueslerReiss_transpose_cdf {lam : ℝ} (hlam : 0 < lam) (u v : ↑unitInterval) : (hueslerReiss lam hlam).cdf ![u, v] = (hueslerReiss lam hlam).cdf ![v, u]

The Hüsler–Reiss copula is exchangeable: A(1 - t) = A(t).