← Copula mathematical handbook

Algebraic properties of bivariate Archimedean copulas

Nelsen, An Introduction to Copulas, second edition, Theorem 4.1.5: a bivariate Archimedean copula C(u, v) = ψ(φ(u) + φ(v)) is

1. symmetric, C(u, v) = C(v, u) (BivariateGenerator.op_comm);
2. associative, C(C(u, v), w) = C(u, C(v, w)) (BivariateGenerator.op_assoc);
3. unchanged when the generator φ is replaced by c φ for a constant c > 0 (BivariateGenerator.scale, BivariateGenerator.scale_copula).

To state associativity, BivariateGenerator.op regards the copula as a binary operation on the unit interval. Associativity holds for strict and non-strict generators alike: the zero set is handled by the key identity C(u, ψ(s)) = ψ(φ(u) + s) (BivariateGenerator.cdf_toI), which is also valid when ψ(s) = 0. The operation has neutral element 1 and absorbing element 0, so (I, op) is a commutative ordered monoid (Nelsen, Section 4.1, the discussion before Theorem 4.1.6).

theorem ProbabilityTheory.Copula.BivariateGenerator.cdf_le_right (g : BivariateGenerator) (u v : ↑unitInterval) : g.cdf u v ≤ ↑v

The Archimedean formula is bounded by its second argument.

theorem ProbabilityTheory.Copula.BivariateGenerator.cdf_le_left (g : BivariateGenerator) (u v : ↑unitInterval) : g.cdf u v ≤ ↑u

The Archimedean formula is bounded by its first argument.

noncomputable def ProbabilityTheory.Copula.BivariateGenerator.op (g : BivariateGenerator) (u v : ↑unitInterval) : ↑unitInterval

The bivariate Archimedean copula as a binary operation on the unit interval.

Equations

• g.op u v = ⟨g.cdf u v, ⋯⟩

@[simp]

theorem ProbabilityTheory.Copula.BivariateGenerator.coe_op (g : BivariateGenerator) (u v : ↑unitInterval) : ↑(g.op u v) = g.cdf u v

theorem ProbabilityTheory.Copula.BivariateGenerator.coe_op_eq_cdf_copula (g : BivariateGenerator) (u v : ↑unitInterval) : ↑(g.op u v) = g.copula.cdf ![u, v]

The operation is the copula CDF at the pair (u, v).

theorem ProbabilityTheory.Copula.BivariateGenerator.op_comm (g : BivariateGenerator) (u v : ↑unitInterval) : g.op u v = g.op v u

Nelsen, Theorem 4.1.5 (1): Archimedean copulas are symmetric.

@[simp]

theorem ProbabilityTheory.Copula.BivariateGenerator.op_one_left (g : BivariateGenerator) (v : ↑unitInterval) : g.op 1 v = v

@[simp]

theorem ProbabilityTheory.Copula.BivariateGenerator.op_one_right (g : BivariateGenerator) (u : ↑unitInterval) : g.op u 1 = u

@[simp]

theorem ProbabilityTheory.Copula.BivariateGenerator.op_zero_left (g : BivariateGenerator) (v : ↑unitInterval) : g.op 0 v = 0

@[simp]

theorem ProbabilityTheory.Copula.BivariateGenerator.op_zero_right (g : BivariateGenerator) (u : ↑unitInterval) : g.op u 0 = 0

theorem ProbabilityTheory.Copula.BivariateGenerator.op_mono_left (g : BivariateGenerator) (v : ↑unitInterval) : Monotone fun (u : ↑unitInterval) => g.op u v

The operation is monotone in each argument.

theorem ProbabilityTheory.Copula.BivariateGenerator.op_mono_right (g : BivariateGenerator) (u : ↑unitInterval) : Monotone fun (v : ↑unitInterval) => g.op u v

theorem ProbabilityTheory.Copula.BivariateGenerator.cdf_toI (g : BivariateGenerator) {u : ↑unitInterval} (hu : u ≠ 0) {s : ℝ} (hs : 0 ≤ s) : g.cdf u (g.toI hs) = g.toFun (g.invFun u + s)

The key identity C(u, ψ(s)) = ψ(φ(u) + s) for u > 0 and s ≥ 0, including the case ψ(s) = 0 of a non-strict generator.

theorem ProbabilityTheory.Copula.BivariateGenerator.op_eq_toI (g : BivariateGenerator) {u v : ↑unitInterval} (hu : u ≠ 0) (hv : v ≠ 0) : g.op u v = g.toI ⋯

For positive arguments the operation is ψ(φ(u) + φ(v)), as a point of I.

theorem ProbabilityTheory.Copula.BivariateGenerator.cdf_op_left (g : BivariateGenerator) {u v w : ↑unitInterval} (hu : u ≠ 0) (hv : v ≠ 0) (hw : w ≠ 0) : g.cdf (g.op u v) w = g.toFun (g.invFun u + g.invFun v + g.invFun w)

Nelsen, Theorem 4.1.5 (2), at the level of the CDF formula: C(C(u, v), w) = ψ(φ(u) + φ(v) + φ(w)) for positive arguments.

theorem ProbabilityTheory.Copula.BivariateGenerator.op_assoc (g : BivariateGenerator) (u v w : ↑unitInterval) : g.op (g.op u v) w = g.op u (g.op v w)

Nelsen, Theorem 4.1.5 (2): Archimedean copulas are associative.

noncomputable def ProbabilityTheory.Copula.BivariateGenerator.scale (g : BivariateGenerator) (c : ℝ) (hc : 0 < c) : BivariateGenerator

Scaling Nelsen's generator: the generator c φ with inverse generator t ↦ ψ(t / c).

Equations

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

@[simp]

theorem ProbabilityTheory.Copula.BivariateGenerator.scale_toFun (g : BivariateGenerator) (c : ℝ) (hc : 0 < c) (t : ℝ) : (g.scale c hc).toFun t = g.toFun (t / c)

@[simp]

theorem ProbabilityTheory.Copula.BivariateGenerator.scale_invFun (g : BivariateGenerator) (c : ℝ) (hc : 0 < c) (u : ↑unitInterval) : (g.scale c hc).invFun u = c * g.invFun u

theorem ProbabilityTheory.Copula.BivariateGenerator.scale_cdf (g : BivariateGenerator) (c : ℝ) (hc : 0 < c) (u v : ↑unitInterval) : (g.scale c hc).cdf u v = g.cdf u v

@[simp]

theorem ProbabilityTheory.Copula.BivariateGenerator.scale_copula (g : BivariateGenerator) (c : ℝ) (hc : 0 < c) : (g.scale c hc).copula = g.copula

Nelsen, Theorem 4.1.5 (3): for c > 0, the generator c φ generates the same copula.

theorem ProbabilityTheory.Copula.IsArchimedean.cdf_assoc {C : Copula 2} (hC : C.IsArchimedean) (u v w : ↑unitInterval) : ∃ (x : ↑unitInterval) (y : ↑unitInterval), ↑x = C.cdf ![u, v] ∧ ↑y = C.cdf ![v, w] ∧ C.cdf ![x, w] = C.cdf ![u, y]

Nelsen, Theorem 4.1.5 (2) for a bivariate copula with an identified generator: C(C(u, v), w) = C(u, C(v, w)), written with CDF values.