Documentation

Copula.Archimedean.Theory

← Copula mathematical handbook

Generic theory of bivariate Archimedean generators #

Consequences of the axioms of BivariateGenerator used in Nelsen, An Introduction to Copulas, second edition, Section 4.1 (the representation C(u, v) = ψ(φ(u) + φ(v)) and its immediate consequences): the inverse generator ψ is strictly decreasing where it is positive, the generator φ inverts ψ on its positive range (φ(C(u, v)) = φ(u) + φ(v) when C(u, v) > 0), and C(u, v) < u whenever 0 < u and 0 < v < 1.

source
theorem ProbabilityTheory.Copula.BivariateGenerator.toFun_zero (g : BivariateGenerator) :
g.toFun 0 = 1

The inverse generator takes the value one at zero.

source
theorem ProbabilityTheory.Copula.BivariateGenerator.antitone_nonneg (g : BivariateGenerator) {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a ≤ b) :
g.toFun b ≤ g.toFun a

The inverse generator is antitone on nonnegative arguments (with plain 0 ≤ _ hypotheses instead of membership in Ici 0).

source
theorem ProbabilityTheory.Copula.BivariateGenerator.toFun_le_one (g : BivariateGenerator) {s : ℝ} (hs : 0 ≤ s) :
g.toFun s ≤ 1

The inverse generator is at most one on nonnegative arguments.

source
theorem ProbabilityTheory.Copula.BivariateGenerator.toFun_lt_of_lt (g : BivariateGenerator) {a b : ℝ} (ha : 0 ≤ a) (hab : a < b) (hb : 0 < g.toFun b) :
g.toFun b < g.toFun a

The inverse generator is strictly decreasing wherever it is positive: if 0 ≤ a < b and ψ b > 0 then ψ b < ψ a.

source
noncomputable def ProbabilityTheory.Copula.BivariateGenerator.toI (g : BivariateGenerator) {s : ℝ} (hs : 0 ≤ s) :
↑unitInterval

The value ψ(s) of the inverse generator at a nonnegative argument, as a point of I.

Equations
Instances For
    source
    @[simp]
    theorem ProbabilityTheory.Copula.BivariateGenerator.coe_toI (g : BivariateGenerator) {s : ℝ} (hs : 0 ≤ s) :
    ↑(g.toI hs) = g.toFun s
    source
    theorem ProbabilityTheory.Copula.BivariateGenerator.toI_ne_zero (g : BivariateGenerator) {s : ℝ} (hs : 0 ≤ s) (hpos : 0 < g.toFun s) :
    g.toI hs ≠ 0
    source
    theorem ProbabilityTheory.Copula.BivariateGenerator.invFun_toI (g : BivariateGenerator) {s : ℝ} (hs : 0 ≤ s) (hpos : 0 < g.toFun s) :
    g.invFun (g.toI hs) = s

    The generator inverts the inverse generator on its positive range: φ(ψ(s)) = s whenever s ≥ 0 and ψ(s) > 0 (Nelsen, Section 4.1).

    source
    theorem ProbabilityTheory.Copula.BivariateGenerator.invFun_cdf (g : BivariateGenerator) {u v : ↑unitInterval} (hu : u ≠ 0) (hv : v ≠ 0) (hpos : 0 < g.cdf u v) :
    ∃ (w : ↑unitInterval), ↑w = g.cdf u v ∧ g.invFun w = g.invFun u + g.invFun v

    Nelsen's identity φ(C(u,v)) = φ(u) + φ(v) whenever C(u,v) > 0.

    source
    theorem ProbabilityTheory.Copula.BivariateGenerator.invFun_pos (g : BivariateGenerator) {v : ↑unitInterval} (hv0 : v ≠ 0) (hv1 : v ≠ 1) :
    0 < g.invFun v

    The generator is strictly positive at every point of (0,1).

    source
    theorem ProbabilityTheory.Copula.BivariateGenerator.cdf_lt_left (g : BivariateGenerator) {u v : ↑unitInterval} (hu : u ≠ 0) (hv : v ≠ 0) (hv1 : v ≠ 1) :
    g.cdf u v < ↑u

    C(u,v) < u for u > 0 and 0 < v < 1 (Nelsen, Section 4.1).

    source
    theorem ProbabilityTheory.Copula.BivariateGenerator.cdf_lt_right (g : BivariateGenerator) {u v : ↑unitInterval} (hu : u ≠ 0) (hu1 : u ≠ 1) (hv : v ≠ 0) :
    g.cdf u v < ↑v

    C(u,v) < v for v > 0 and 0 < u < 1.

    source
    theorem ProbabilityTheory.Copula.HasArchimedeanGenerator.eq_copula {C : Copula 2} {g : BivariateGenerator} (h : C.HasArchimedeanGenerator g) :
    C = g.copula

    A copula with generator g in the sense of HasArchimedeanGenerator is g.copula.

    source
    theorem ProbabilityTheory.Copula.IsArchimedean.exists_generator_copula {C : Copula 2} (h : C.IsArchimedean) :
    ∃ (g : BivariateGenerator), C = g.copula

    A bivariate Archimedean copula is the copula of some BivariateGenerator.