← Copula mathematical handbook

Ali–Mikhail–Haq copulas on the full bivariate parameter interval

noncomputable def ProbabilityTheory.Copula.amhGenerator (θ : ℝ) (hmin : -1 ≤ θ) (hmax : θ < 1) : BivariateGenerator

The Ali–Mikhail–Haq inverse generator for parameters below one.

Equations

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

noncomputable def ProbabilityTheory.Copula.amh (θ : ℝ) (hmin : -1 ≤ θ) (hmax : θ ≤ 1) : Copula 2

The Ali–Mikhail–Haq family on its complete bivariate parameter interval.

Equations

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

@[simp]

theorem ProbabilityTheory.Copula.amh_one (hmin : -1 ≤ 1) : amh 1 hmin ⋯ = clayton 2 1 ⋯

theorem ProbabilityTheory.Copula.amh_isArchimedean_of_lt_one (θ : ℝ) (hmin : -1 ≤ θ) (hmax : θ ≤ 1) (hθ : θ < 1) : (amh θ hmin hmax).IsArchimedean

theorem ProbabilityTheory.Copula.amhGenerator_cdf (θ : ℝ) (hmin : -1 ≤ θ) (hmax : θ < 1) (a b : ↑unitInterval) (ha : a ≠ 0) (hb : b ≠ 0) : (amhGenerator θ hmin hmax).cdf a b = ↑a * ↑b / (1 - θ * (1 - ↑a) * (1 - ↑b))

The standard rational AMH CDF on positive coordinates.

theorem ProbabilityTheory.Copula.cdf_amh_of_lt_one (θ : ℝ) (hmin : -1 ≤ θ) (hmax : θ ≤ 1) (hθ : θ < 1) (a b : ↑unitInterval) (ha : a ≠ 0) (hb : b ≠ 0) : (amh θ hmin hmax).cdf ![a, b] = ↑a * ↑b / (1 - θ * (1 - ↑a) * (1 - ↑b))

The rational AMH formula for every parameter strictly below one.

theorem ProbabilityTheory.Copula.cdf_amh_lt_one (θ : ℝ) (hmin : -1 ≤ θ) (hmax : θ ≤ 1) (hθ : θ < 1) (a b : ↑unitInterval) : (amh θ hmin hmax).cdf ![a, b] = ↑a * ↑b / (1 - θ * (1 - ↑a) * (1 - ↑b))

The rational AMH CDF on the entire closed square below the endpoint.

theorem ProbabilityTheory.Copula.cdf_amh_one_of_pos (a b : ↑unitInterval) (ha : 0 < ↑a) (hb : 0 < ↑b) : (amh 1 ⋯ ⋯).cdf ![a, b] = ↑a * ↑b / (1 - (1 - ↑a) * (1 - ↑b))

The AMH endpoint θ=1 has the Clayton(1) rational CDF on positive coordinates.

theorem ProbabilityTheory.Copula.cdf_amh_one (a b : ↑unitInterval) : (amh 1 ⋯ ⋯).cdf ![a, b] = ↑a * ↑b / (1 - (1 - ↑a) * (1 - ↑b))

The rational AMH endpoint formula on the closed square.

theorem ProbabilityTheory.Copula.cdf_amh (θ : ℝ) (hmin : -1 ≤ θ) (hmax : θ ≤ 1) (a b : ↑unitInterval) : (amh θ hmin hmax).cdf ![a, b] = ↑a * ↑b / (1 - θ * (1 - ↑a) * (1 - ↑b))

The exact AMH CDF for the full bivariate parameter interval and closed square.

theorem ProbabilityTheory.Copula.isArchimedean_amh (θ : ℝ) (hmin : -1 ≤ θ) (hmax : θ ≤ 1) : (amh θ hmin hmax).IsArchimedean

Every bivariate AMH member is Archimedean, including the Clayton endpoint.

@[simp]

theorem ProbabilityTheory.Copula.amh_zero : amh 0 ⋯ ⋯ = independence 2

The zero-parameter AMH copula is independence, including all boundaries.