← Copula mathematical handbook

Bivariate Gumbel–Hougaard (logistic extreme-value) copulas

noncomputable def ProbabilityTheory.Copula.gumbelGenerator (θ : ℝ) (hθ : 1 ≤ θ) : BivariateGenerator

Gumbel's inverse generator exp(-t^(1/θ)).

Equations

• ProbabilityTheory.Copula.gumbelGenerator θ hθ = ProbabilityTheory.Copula.exponentialGenerator.outerPower θ hθ

noncomputable def ProbabilityTheory.Copula.gumbel (θ : ℝ) (hθ : 1 ≤ θ) : Copula 2

The bivariate Gumbel–Hougaard copula, including independence at θ = 1.

Equations

• ProbabilityTheory.Copula.gumbel θ hθ = (ProbabilityTheory.Copula.gumbelGenerator θ hθ).copula

theorem ProbabilityTheory.Copula.isArchimedean_gumbel (θ : ℝ) (hθ : 1 ≤ θ) : (gumbel θ hθ).IsArchimedean

theorem ProbabilityTheory.Copula.cdf_gumbel (θ : ℝ) (hθ : 1 ≤ θ) (u : Fin 2 → ↑unitInterval) (hu : ∀ (i : Fin 2), u i ≠ 0) : (gumbel θ hθ).cdf u = Real.exp (-((-Real.log ↑(u 0)) ^ θ + (-Real.log ↑(u 1)) ^ θ) ^ θ⁻¹)

@[simp]

theorem ProbabilityTheory.Copula.gumbel_one : gumbel 1 ⋯ = independence 2

theorem ProbabilityTheory.Copula.isExtremeValue_gumbel (θ : ℝ) (hθ : 1 ≤ θ) : (gumbel θ hθ).IsExtremeValue

noncomputable def ProbabilityTheory.Copula.tawn (θ : ℝ) (hθ : 1 ≤ θ) (α β : ↑unitInterval) : Copula 2

An asymmetric logistic (Tawn) copula with two weights and θ ≥ 1.

Equations

• ProbabilityTheory.Copula.tawn θ hθ α β = (ProbabilityTheory.Copula.gumbel θ hθ).maxProduct (ProbabilityTheory.Copula.independence 2) ![α, β]

theorem ProbabilityTheory.Copula.isExtremeValue_tawn (θ : ℝ) (hθ : 1 ≤ θ) (α β : ↑unitInterval) : (tawn θ hθ α β).IsExtremeValue

theorem ProbabilityTheory.Copula.gumbel_cdf_full (θ : ℝ) (hθ : 1 ≤ θ) (u v : ↑unitInterval) : (gumbel θ hθ).cdf ![u, v] = if u = 0 ∨ v = 0 then 0 else Real.exp (-((-Real.log ↑u) ^ θ + (-Real.log ↑v) ^ θ) ^ θ⁻¹)

Table 1's Gumbel–Hougaard CDF on the whole closed square. The paper's logarithmic expression applies to positive coordinates; copula groundedness supplies the values on the two zero axes.

theorem ProbabilityTheory.Copula.tawn_cdf_positive (θ : ℝ) (hθ : 1 ≤ θ) (α β u v : ↑unitInterval) (hu : u ≠ 0) (hv : v ≠ 0) : (tawn θ hθ α β).cdf ![u, v] = ↑u ^ (1 - ↑α) * ↑v ^ (1 - ↑β) * Real.exp (-((↑α * -Real.log ↑u) ^ θ + (↑β * -Real.log ↑v) ^ θ) ^ θ⁻¹)

Table 1's Tawn CDF at positive coordinates, with all finite shape and weight endpoints included.

theorem ProbabilityTheory.Copula.tawn_cdf_full (θ : ℝ) (hθ : 1 ≤ θ) (α β u v : ↑unitInterval) : (tawn θ hθ α β).cdf ![u, v] = if u = 0 ∨ v = 0 then 0 else ↑u ^ (1 - ↑α) * ↑v ^ (1 - ↑β) * Real.exp (-((↑α * -Real.log ↑u) ^ θ + (↑β * -Real.log ↑v) ^ θ) ^ θ⁻¹)

The Tawn formula on the closed square, making its zero-axis extension explicit rather than applying log 0 in the paper's analytic notation.

theorem ProbabilityTheory.Copula.tawn_zero_zero (θ : ℝ) (hθ : 1 ≤ θ) : tawn θ hθ 0 0 = independence 2

Both zero Tawn weights give independence, for every admissible shape.

theorem ProbabilityTheory.Copula.tawn_one_one (θ : ℝ) (hθ : 1 ≤ θ) : tawn θ hθ 1 1 = gumbel θ hθ

Both unit Tawn weights recover the Gumbel–Hougaard copula.

theorem ProbabilityTheory.Copula.tawn_zero_left (θ : ℝ) (hθ : 1 ≤ θ) (β : ↑unitInterval) : tawn θ hθ 0 β = independence 2

theorem ProbabilityTheory.Copula.tawn_zero_right (θ : ℝ) (hθ : 1 ≤ θ) (α : ↑unitInterval) : tawn θ hθ α 0 = independence 2

theorem ProbabilityTheory.Copula.tawn_shape_one (α β : ↑unitInterval) : tawn 1 ⋯ α β = independence 2