← Mathematical handbook

Joe source CDF on the closed square

theorem Papers.AnsariRockel2024.joe_cdf_full (θ : ℝ) (hθ : 1 ≤ θ) (u v : ↑unitInterval) : (ProbabilityTheory.Copula.joe θ hθ).cdf ![u, v] = if u = 0 ∨ v = 0 then 0 else 1 - ((1 - ↑u) ^ θ + (1 - ↑v) ^ θ - (1 - ↑u) ^ θ * (1 - ↑v) ^ θ) ^ θ⁻¹

Table 1's Joe CDF, with grounded zero-axis values made explicit.

theorem Papers.AnsariRockel2024.joe_one : ProbabilityTheory.Copula.joe 1 ⋯ = ProbabilityTheory.Copula.independence 2

Table 2's independence endpoint for Joe.

theorem Papers.AnsariRockel2024.frank_positive_cdf_full (θ : ℝ) (hθ : 0 < θ) (u v : ↑unitInterval) : (ProbabilityTheory.Copula.frank θ hθ).cdf ![u, v] = if u = 0 ∨ v = 0 then 0 else -Real.log (1 - (1 - Real.exp (-θ * ↑u)) * (1 - Real.exp (-θ * ↑v)) / (1 - Real.exp (-θ))) / θ

Table 1's Frank CDF for the positive parameter branch, including grounded zero axes. The negative branch and zero case are proved below.

theorem Papers.AnsariRockel2024.frank_negative_cdf_reflected (θ : ℝ) (hθ : θ < 0) (u v : ↑unitInterval) : (ProbabilityTheory.Copula.frankNegative θ hθ).cdf ![u, v] = ↑u - if u = 0 ∨ unitInterval.symm v = 0 then 0 else -Real.log (1 - (1 - Real.exp (θ * ↑u)) * (1 - Real.exp (θ * ↑(unitInterval.symm v))) / (1 - Real.exp θ)) / -θ

The negative Frank branch as an exact reflected CDF on the closed square. The printed logarithmic form is proved separately below.

theorem Papers.AnsariRockel2024.frank_negative_cdf_source (θ : ℝ) (hθ : θ < 0) (u v : ↑unitInterval) : (ProbabilityTheory.Copula.frankNegative θ hθ).cdf ![u, v] = -Real.log (1 + (Real.exp (-θ * ↑u) - 1) * (Real.exp (-θ * ↑v) - 1) / (Real.exp (-θ) - 1)) / θ

Table 1's printed negative-parameter Frank CDF, including every boundary point.

theorem Papers.AnsariRockel2024.amh_cdf_full (θ : ℝ) (hmin : -1 ≤ θ) (hmax : θ ≤ 1) (u v : ↑unitInterval) : (ProbabilityTheory.Copula.amh θ hmin hmax).cdf ![u, v] = ↑u * ↑v / (1 - θ * (1 - ↑u) * (1 - ↑v))

Table 2's Ali–Mikhail–Haq CDF on the full parameter interval and closed square.

theorem Papers.AnsariRockel2024.frank_zero_cdf (u v : ↑unitInterval) : (ProbabilityTheory.Copula.independence 2).cdf ![u, v] = ↑u * ↑v

Table 1's Frank family at its zero parameter is independence.

theorem Papers.AnsariRockel2024.nelsen2_cdf_full (θ : ℝ) (hθ : 1 ≤ θ) (u v : ↑unitInterval) : (ProbabilityTheory.Copula.nelsen2 θ hθ).cdf ![u, v] = if u = 0 ∨ v = 0 then 0 else max 0 (1 - ((1 - ↑u) ^ θ + (1 - ↑v) ^ θ) ^ θ⁻¹)

Table 1's Nelsen 2 CDF on the closed square.

theorem Papers.AnsariRockel2024.nelsen8_cdf_full (θ : ℝ) (hθ : 1 ≤ θ) (u v : ↑unitInterval) : (ProbabilityTheory.Copula.nelsen8 θ hθ).cdf ![u, v] = max 0 ((θ ^ 2 * ↑u * ↑v - (1 - ↑u) * (1 - ↑v)) / (θ ^ 2 - (θ - 1) ^ 2 * (1 - ↑u) * (1 - ↑v)))

Table 1's printed Nelsen 8 rational CDF on the entire closed square.

theorem Papers.AnsariRockel2024.genestGhoudi_cdf_full (θ : ℝ) (hθ : 1 ≤ θ) (u v : ↑unitInterval) : (ProbabilityTheory.Copula.genestGhoudi θ hθ).cdf ![u, v] = if u = 0 ∨ v = 0 then 0 else max 0 (1 - ((1 - ↑u ^ θ⁻¹) ^ θ + (1 - ↑v ^ θ⁻¹) ^ θ) ^ θ⁻¹) ^ θ

Table 1's Genest–Ghoudi (Nelsen 15) CDF on the closed square.

theorem Papers.AnsariRockel2024.nelsen12_cdf_full (θ : ℝ) (hθ : 1 ≤ θ) (u v : ↑unitInterval) : (ProbabilityTheory.Copula.nelsen12 θ hθ).cdf ![u, v] = if u = 0 ∨ v = 0 then 0 else (1 + (((↑u)⁻¹ - 1) ^ θ + ((↑v)⁻¹ - 1) ^ θ) ^ θ⁻¹)⁻¹

Table 1's Nelsen 12 CDF on the closed square.

theorem Papers.AnsariRockel2024.nelsen14_cdf_full (θ : ℝ) (hθ : 1 ≤ θ) (u v : ↑unitInterval) : (ProbabilityTheory.Copula.nelsen14 θ hθ).cdf ![u, v] = if u = 0 ∨ v = 0 then 0 else (1 + ((↑u ^ (-θ⁻¹) - 1) ^ θ + (↑v ^ (-θ⁻¹) - 1) ^ θ) ^ θ⁻¹) ^ (-θ)

Table 1's Nelsen 14 CDF on the closed square.

theorem Papers.AnsariRockel2024.nelsen2_one : ProbabilityTheory.Copula.nelsen2 1 ⋯ = ProbabilityTheory.Copula.countermonotonic

Table 2's lower Fréchet endpoint of Nelsen 2.

theorem Papers.AnsariRockel2024.nelsen8_one : ProbabilityTheory.Copula.nelsen8 1 ⋯ = ProbabilityTheory.Copula.countermonotonic

Table 2's lower Fréchet endpoint of Nelsen 8.

theorem Papers.AnsariRockel2024.genestGhoudi_one : ProbabilityTheory.Copula.genestGhoudi 1 ⋯ = ProbabilityTheory.Copula.countermonotonic

Table 2's lower Fréchet endpoint of Genest–Ghoudi.

theorem Papers.AnsariRockel2024.nelsen12_one : ProbabilityTheory.Copula.nelsen12 1 ⋯ = ProbabilityTheory.Copula.clayton 2 1 ⋯

Table 2's Clayton specialization of Nelsen 12.

theorem Papers.AnsariRockel2024.nelsen14_one : ProbabilityTheory.Copula.nelsen14 1 ⋯ = ProbabilityTheory.Copula.clayton 2 1 ⋯

Table 2's Clayton specialization of Nelsen 14.