← Mathematical handbook

Numbered Archimedean families from Nelsen

The numbering follows Table 2 of Ansari and Rockel (arXiv:2310.17307v3). All constructors return proved copula measures. Formulas are stated on positive coordinates; the common groundedness theorem supplies the zero boundary.

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

Nelsen's family 2, including the lower Fréchet bound at one.

Equations

• ProbabilityTheory.Copula.nelsen2 θ hθ = (ProbabilityTheory.Copula.truncatedLinearGenerator.outerPower θ hθ).copula

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

Genest–Ghoudi (Nelsen's family 15).

Equations

• ProbabilityTheory.Copula.genestGhoudi θ hθ = ((ProbabilityTheory.Copula.truncatedLinearGenerator.outerPower θ hθ).innerPower θ hθ).copula

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

Nelsen's family 12 is the θ = 1 subfamily of BB1.

Equations

• ProbabilityTheory.Copula.nelsen12 θ hθ = ProbabilityTheory.Copula.bb1 1 ProbabilityTheory.Copula.nelsen12._proof_1 θ hθ

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

Nelsen's family 14 is the reciprocal-parameter subfamily of BB1.

Equations

• ProbabilityTheory.Copula.nelsen14 θ hθ = ProbabilityTheory.Copula.bb1 θ⁻¹ ⋯ θ hθ

theorem ProbabilityTheory.Copula.isArchimedean_nelsen2 (θ : ℝ) (hθ : 1 ≤ θ) : (nelsen2 θ hθ).IsArchimedean

theorem ProbabilityTheory.Copula.isArchimedean_genestGhoudi (θ : ℝ) (hθ : 1 ≤ θ) : (genestGhoudi θ hθ).IsArchimedean

theorem ProbabilityTheory.Copula.isArchimedean_nelsen12 (θ : ℝ) (hθ : 1 ≤ θ) : (nelsen12 θ hθ).IsArchimedean

theorem ProbabilityTheory.Copula.isArchimedean_nelsen14 (θ : ℝ) (hθ : 1 ≤ θ) : (nelsen14 θ hθ).IsArchimedean

theorem ProbabilityTheory.Copula.cdf_nelsen2 (θ : ℝ) (hθ : 1 ≤ θ) (u : Fin 2 → ↑unitInterval) (hu : ∀ (i : Fin 2), u i ≠ 0) : (nelsen2 θ hθ).cdf u = max 0 (1 - ((1 - ↑(u 0)) ^ θ + (1 - ↑(u 1)) ^ θ) ^ θ⁻¹)

theorem ProbabilityTheory.Copula.cdf_genestGhoudi (θ : ℝ) (hθ : 1 ≤ θ) (u : Fin 2 → ↑unitInterval) (hu : ∀ (i : Fin 2), u i ≠ 0) : (genestGhoudi θ hθ).cdf u = max 0 (1 - ((1 - ↑(u 0) ^ θ⁻¹) ^ θ + (1 - ↑(u 1) ^ θ⁻¹) ^ θ) ^ θ⁻¹) ^ θ

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem ProbabilityTheory.Copula.nelsen2_cdf_full (θ : ℝ) (hθ : 1 ≤ θ) (u v : ↑unitInterval) : (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 ProbabilityTheory.Copula.genestGhoudi_cdf_full (θ : ℝ) (hθ : 1 ≤ θ) (u v : ↑unitInterval) : (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 ProbabilityTheory.Copula.nelsen12_cdf_full (θ : ℝ) (hθ : 1 ≤ θ) (u v : ↑unitInterval) : (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 ProbabilityTheory.Copula.nelsen14_cdf_full (θ : ℝ) (hθ : 1 ≤ θ) (u v : ↑unitInterval) : (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.