← Copula mathematical handbook

The Nelsen 8 bivariate copula

A rational non-strict Archimedean generator is valid for θ ≥ 1. The printed CDF holds on the entire closed square, and θ = 1 gives the lower Fréchet bound.

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

Equations

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

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

Nelsen 8 as a valid bivariate Archimedean copula for θ ≥ 1.

Equations

• ProbabilityTheory.Copula.nelsen8 θ hθ = (ProbabilityTheory.Copula.nelsen8Generator θ hθ).copula

theorem ProbabilityTheory.Copula.isArchimedean_nelsen8 (θ : ℝ) (hθ : 1 ≤ θ) : (nelsen8 θ hθ).IsArchimedean

theorem ProbabilityTheory.Copula.n8_source_den_pos (θ u v : ℝ) (hθ : 1 ≤ θ) (hu : 0 ≤ u) (_hu1 : u ≤ 1) (hv : 0 ≤ v) (hv1 : v ≤ 1) : 0 < θ ^ 2 - (θ - 1) ^ 2 * (1 - u) * (1 - v)

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

The printed Nelsen 8 CDF on the full closed unit square.

@[simp]

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

Nelsen 8 starts at the lower Fréchet copula.

theorem ProbabilityTheory.Copula.lowerOrthantLE_nelsen8 {θ η : ℝ} (hθ : 1 ≤ θ) (hη : 1 ≤ η) (hθη : θ ≤ η) : (nelsen8 θ hθ).LowerOrthantLE (nelsen8 η hη)

Nelsen 8 increases in lower-orthant order with its parameter.