← Mathematical handbook

Fréchet and Mardia mixture families

noncomputable def ProbabilityTheory.Copula.frechet (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b ≤ 1) : Copula 2

The bivariate Fréchet family: weights a, b, and 1-a-b on M, W, and Π.

Equations

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

theorem ProbabilityTheory.Copula.cdf_frechet (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b ≤ 1) (u : Fin 2 → ↑unitInterval) : (frechet a b ha hb hab).cdf u = a * (comonotonic 2).cdf u + b * countermonotonic.cdf u + (1 - a - b) * (independence 2).cdf u

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

Mardia's one-parameter family, for θ ∈ [-1,1].

Equations

• ProbabilityTheory.Copula.mardia θ hθ = ProbabilityTheory.Copula.frechet (θ ^ 2 * (1 + θ) / 2) (θ ^ 2 * (1 - θ) / 2) ⋯ ⋯ ⋯

@[simp]

theorem ProbabilityTheory.Copula.mardia_zero : mardia 0 ⋯ = independence 2

@[simp]

theorem ProbabilityTheory.Copula.mardia_one : mardia 1 ⋯ = comonotonic 2

@[simp]

theorem ProbabilityTheory.Copula.mardia_neg_one : mardia (-1) ⋯ = countermonotonic