Documentation

Copula.Families.Joe

← Mathematical handbook

Bivariate Joe and BB6 (Joe–Gumbel) copulas #

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

Joe's inverse generator 1-(1-exp(-t))^(1/θ), for θ ≥ 1.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def ProbabilityTheory.Copula.joe (θ : ℝ) (hθ : 1 ≤ θ) :
    Copula 2

    The bivariate Joe family.

    Equations
    Instances For
      source
      theorem ProbabilityTheory.Copula.isArchimedean_joe (θ : ℝ) (hθ : 1 ≤ θ) :
      (joe θ hθ).IsArchimedean
      source
      theorem ProbabilityTheory.Copula.cdf_joe (θ : ℝ) (hθ : 1 ≤ θ) (u : Fin 2 → ↑unitInterval) (hu : ∀ (i : Fin 2), u i ≠ 0) :
      (joe θ hθ).cdf u = 1 - (1 - (1 - (1 - ↑(u 0)) ^ θ) * (1 - (1 - ↑(u 1)) ^ θ)) ^ θ⁻¹
      source
      theorem ProbabilityTheory.Copula.joe_cdf_full (θ : ℝ) (hθ : 1 ≤ θ) (u v : ↑unitInterval) :
      (joe θ hθ).cdf ![u, v] = if u = 0 ∨ v = 0 then 0 else 1 - ((1 - ↑u) ^ θ + (1 - ↑v) ^ θ - (1 - ↑u) ^ θ * (1 - ↑v) ^ θ) ^ θ⁻¹

      Table 1's Joe CDF, with grounded zero-axis values made explicit.

      source
      noncomputable def ProbabilityTheory.Copula.bb6 (θ : ℝ) (hθ : 1 ≤ θ) (δ : ℝ) (hδ : 1 ≤ δ) :
      Copula 2

      BB6 (Joe–Gumbel), including Joe when the outer-power parameter is one.

      Equations
      Instances For
        source
        theorem ProbabilityTheory.Copula.isArchimedean_bb6 (θ : ℝ) (hθ : 1 ≤ θ) (δ : ℝ) (hδ : 1 ≤ δ) :
        (bb6 θ hθ δ hδ).IsArchimedean
        source
        @[simp]
        theorem ProbabilityTheory.Copula.bb6_one (θ : ℝ) (hθ : 1 ≤ θ) :
        bb6 θ hθ 1 ⋯ = joe θ hθ
        source
        @[simp]
        theorem ProbabilityTheory.Copula.joe_one :
        joe 1 ⋯ = independence 2
        source
        theorem ProbabilityTheory.Copula.cdf_bb6 (θ : ℝ) (hθ : 1 ≤ θ) (δ : ℝ) (hδ : 1 ≤ δ) (u : Fin 2 → ↑unitInterval) (hu : ∀ (i : Fin 2), u i ≠ 0) :
        (bb6 θ hθ δ hδ).cdf u = 1 - (1 - Real.exp (-((-Real.log (1 - (1 - ↑(u 0)) ^ θ)) ^ δ + (-Real.log (1 - (1 - ↑(u 1)) ^ θ)) ^ δ) ^ δ⁻¹)) ^ θ⁻¹
        source
        theorem ProbabilityTheory.Copula.bb6_cdf_full (θ : ℝ) (hθ : 1 ≤ θ) (δ : ℝ) (hδ : 1 ≤ δ) (u v : ↑unitInterval) :
        (bb6 θ hθ δ hδ).cdf ![u, v] = if u = 0 ∨ v = 0 then 0 else 1 - (1 - Real.exp (-((-Real.log (1 - (1 - ↑u) ^ θ)) ^ δ + (-Real.log (1 - (1 - ↑v) ^ θ)) ^ δ) ^ δ⁻¹)) ^ θ⁻¹

        The BB6 CDF on the closed square for both parameters at least one. The analytic Joe–Gumbel formula is used only away from the zero axes.