← Copula mathematical handbook

Nelsen's seventh family

The parameter runs from countermonotonicity at zero to independence at one. Its CDF has a zero region, so no positive-density hypothesis is imposed.

noncomputable def ProbabilityTheory.Copula.nelsen7Generator (θ : ℝ) (hθ : 0 < θ) (h1 : θ ≤ 1) : BivariateGenerator

A finite-zero exponential generator, with its linear limiting case handled separately by nelsen7.

Equations

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

noncomputable def ProbabilityTheory.Copula.nelsen7 (θ : ↑unitInterval) : Copula 2

Nelsen 7 on its whole parameter interval.

Equations

• ProbabilityTheory.Copula.nelsen7 θ = if h : θ = 0 then ProbabilityTheory.Copula.countermonotonic else (ProbabilityTheory.Copula.nelsen7Generator ↑θ ⋯ ⋯).copula

theorem ProbabilityTheory.Copula.isArchimedean_nelsen7 (θ : ↑unitInterval) : (nelsen7 θ).IsArchimedean

theorem ProbabilityTheory.Copula.cdf_nelsen7 (θ u v : ↑unitInterval) : (nelsen7 θ).cdf ![u, v] = max 0 (↑θ * ↑u * ↑v + (1 - ↑θ) * (↑u + ↑v - 1))

@[simp]

theorem ProbabilityTheory.Copula.nelsen7_zero : nelsen7 0 = countermonotonic

@[simp]

theorem ProbabilityTheory.Copula.nelsen7_one : nelsen7 1 = independence 2

theorem ProbabilityTheory.Copula.isSD_nelsen7 (θ : ↑unitInterval) : (nelsen7 θ).IsSD

theorem ProbabilityTheory.Copula.isCD_nelsen7 (θ : ↑unitInterval) : (nelsen7 θ).IsCD

theorem ProbabilityTheory.Copula.lowerOrthantLE_nelsen7 {θ η : ↑unitInterval} (h : θ ≤ η) : (nelsen7 θ).LowerOrthantLE (nelsen7 η)

theorem ProbabilityTheory.Copula.isSI_nelsen7_iff (θ : ↑unitInterval) : (nelsen7 θ).IsSI ↔ θ = 1

The sole conditionally increasing member is independence.

theorem ProbabilityTheory.Copula.isCI_nelsen7_iff (θ : ↑unitInterval) : (nelsen7 θ).IsCI ↔ θ = 1