Documentation

Copula.Families.Frank

← Copula mathematical handbook

Positive-parameter bivariate Frank copulas #

The inverse generator is -log(1-(1-exp(-θ))*exp(-t))/θ. This module covers θ > 0; the negative bivariate branch is not asserted here.

source
noncomputable def ProbabilityTheory.Copula.frankGenerator (θ : ℝ) (hθ : 0 < θ) :
BivariateGenerator

Frank's inverse generator, with positive dependence parameter.

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

    The positive-parameter bivariate Frank family.

    Equations
    Instances For
      source
      theorem ProbabilityTheory.Copula.isArchimedean_frank (θ : ℝ) (hθ : 0 < θ) :
      (frank θ hθ).IsArchimedean
      source
      theorem ProbabilityTheory.Copula.cdf_frank (θ : ℝ) (hθ : 0 < θ) (u : Fin 2 → ↑unitInterval) (hu : ∀ (i : Fin 2), u i ≠ 0) :
      (frank θ hθ).cdf u = -Real.log (1 - (1 - Real.exp (-θ * ↑(u 0))) * (1 - Real.exp (-θ * ↑(u 1))) / (1 - Real.exp (-θ))) / θ
      source
      theorem ProbabilityTheory.Copula.frank_cdf_full (θ : ℝ) (hθ : 0 < θ) (u v : ↑unitInterval) :
      (frank θ hθ).cdf ![u, v] = if u = 0 ∨ v = 0 then 0 else -Real.log (1 - (1 - Real.exp (-θ * ↑u)) * (1 - Real.exp (-θ * ↑v)) / (1 - Real.exp (-θ))) / θ

      The positive-parameter Frank CDF on the entire closed unit square. The analytic logarithmic formula is used only away from the grounded zero axes.