← Mathematical handbook

Full-square source CDF for the Gumbel–Hougaard family

theorem Papers.AnsariRockel2024.gumbel_cdf_full (θ : ℝ) (hθ : 1 ≤ θ) (u v : ↑unitInterval) : (ProbabilityTheory.Copula.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 Papers.AnsariRockel2024.gumbel_one : ProbabilityTheory.Copula.gumbel 1 ⋯ = ProbabilityTheory.Copula.independence 2

Table 2's independence endpoint for Gumbel–Hougaard.

theorem Papers.AnsariRockel2024.tawn_cdf_positive (θ : ℝ) (hθ : 1 ≤ θ) (α β u v : ↑unitInterval) (hu : u ≠ 0) (hv : v ≠ 0) : (ProbabilityTheory.Copula.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 Papers.AnsariRockel2024.tawn_cdf_full (θ : ℝ) (hθ : 1 ≤ θ) (α β u v : ↑unitInterval) : (ProbabilityTheory.Copula.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 Papers.AnsariRockel2024.tawn_zero_zero (θ : ℝ) (hθ : 1 ≤ θ) : ProbabilityTheory.Copula.tawn θ hθ 0 0 = ProbabilityTheory.Copula.independence 2

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

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

Both unit Tawn weights recover the Gumbel–Hougaard copula.

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

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

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