← Copula mathematical handbook

Level curves and the zero set of bivariate Archimedean copulas

For C(u, v) = ψ(φ(u) + φ(v)) (Nelsen, An Introduction to Copulas, second edition, Sections 4.1 and 4.3):

• the generator φ is strictly decreasing (BivariateGenerator.invFun_lt_of_lt) and convex on (0, 1] (BivariateGenerator.convexOn_invFunReal);
• for t > 0 the level set C(u, v) = t is the curve φ(u) + φ(v) = φ(t) (BivariateGenerator.cdf_eq_iff), and C(u, v) ≥ t iff φ(u) + φ(v) ≤ φ(t) (BivariateGenerator.le_cdf_iff);
• the level curve v = L_t(u) = ψ(φ(t) − φ(u)), t ≤ u ≤ 1, lies on level t (BivariateGenerator.cdf_levelCurve) and is convex (Nelsen, Theorem 4.3.2, BivariateGenerator.convexOn_levelCurve); equivalently, every upper level set {C ≥ t} is convex (BivariateGenerator.convex_upperLevelSet);
• the zero set C(u, v) = 0 is {u = 0} ∪ {v = 0} ∪ {ψ(φ(u) + φ(v)) = 0} (BivariateGenerator.cdf_eq_zero_iff). A generator is strict (ψ > 0 everywhere, Nelsen's φ(0) = ∞) iff C > 0 on (0, 1]² (BivariateGenerator.isStrict_iff). A non-strict generator has a finite zero S = φ(0) > 0 with ψ > 0 on [0, S) and ψ = 0 on (S, ∞) (BivariateGenerator.exists_zero_threshold), so its diagonal vanishes near zero (BivariateGenerator.exists_diagonal_eq_zero).

noncomputable def ProbabilityTheory.Copula.BivariateGenerator.invFunReal (g : BivariateGenerator) (x : ℝ) : ℝ

The generator φ as a real function, extended constantly outside [0, 1] (its value at 0 is the unused junk value φ(0) of the structure).

Equations

• g.invFunReal x = g.invFun (Set.projIcc 0 1 ProbabilityTheory.Copula.BivariateGenerator.invFunReal._proof_1 x)

@[simp]

theorem ProbabilityTheory.Copula.BivariateGenerator.invFunReal_coe (g : BivariateGenerator) (u : ↑unitInterval) : g.invFunReal ↑u = g.invFun u

def ProbabilityTheory.Copula.BivariateGenerator.IsStrict (g : BivariateGenerator) : Prop

A generator is strict when the inverse generator never vanishes (Nelsen's φ(0) = ∞).

Equations

• g.IsStrict = ∀ (s : ℝ), 0 ≤ s → 0 < g.toFun s

theorem ProbabilityTheory.Copula.BivariateGenerator.coe_pos {u : ↑unitInterval} (hu : u ≠ 0) : 0 < ↑u

theorem ProbabilityTheory.Copula.BivariateGenerator.invFun_lt_of_lt (g : BivariateGenerator) {u v : ↑unitInterval} (hu : u ≠ 0) (huv : u < v) : g.invFun v < g.invFun u

The generator is strictly decreasing on (0, 1].

theorem ProbabilityTheory.Copula.BivariateGenerator.le_toFun_iff (g : BivariateGenerator) {t : ↑unitInterval} (ht : t ≠ 0) {s : ℝ} (hs : 0 ≤ s) : ↑t ≤ g.toFun s ↔ s ≤ g.invFun t

t ≤ ψ(s) iff s ≤ φ(t), for t > 0 and s ≥ 0.

theorem ProbabilityTheory.Copula.BivariateGenerator.le_cdf_iff (g : BivariateGenerator) {t : ↑unitInterval} (ht : t ≠ 0) (u v : ↑unitInterval) : ↑t ≤ g.cdf u v ↔ u ≠ 0 ∧ v ≠ 0 ∧ g.invFun u + g.invFun v ≤ g.invFun t

Upper level sets: for t > 0, t ≤ C(u, v) iff u, v > 0 and φ(u) + φ(v) ≤ φ(t).

theorem ProbabilityTheory.Copula.BivariateGenerator.cdf_eq_iff (g : BivariateGenerator) {t u v : ↑unitInterval} (ht : t ≠ 0) (hu : u ≠ 0) (hv : v ≠ 0) : g.cdf u v = ↑t ↔ g.invFun u + g.invFun v = g.invFun t

Level curves: for t > 0 and u, v > 0, C(u, v) = t iff φ(u) + φ(v) = φ(t).

theorem ProbabilityTheory.Copula.BivariateGenerator.cdf_eq_zero_iff (g : BivariateGenerator) (u v : ↑unitInterval) : g.cdf u v = 0 ↔ u = 0 ∨ v = 0 ∨ g.toFun (g.invFun u + g.invFun v) = 0

The zero set of an Archimedean copula.

theorem ProbabilityTheory.Copula.BivariateGenerator.IsStrict.cdf_pos {g : BivariateGenerator} (hg : g.IsStrict) {u v : ↑unitInterval} (hu : u ≠ 0) (hv : v ≠ 0) : 0 < g.cdf u v

The copula of a strict generator is positive on (0, 1]².

theorem ProbabilityTheory.Copula.BivariateGenerator.exists_zero_threshold (g : BivariateGenerator) (hg : ¬g.IsStrict) : ∃ (S : ℝ), 0 < S ∧ (∀ (s : ℝ), 0 ≤ s → s < S → 0 < g.toFun s) ∧ (∀ (s : ℝ), S < s → g.toFun s = 0) ∧ ∀ (u : ↑unitInterval), u ≠ 0 → g.invFun u ≤ S

A non-strict generator has a positive zero threshold S: ψ > 0 on [0, S), ψ = 0 on (S, ∞), and φ ≤ S on (0, 1] (Nelsen's φ(0) = S < ∞).

theorem ProbabilityTheory.Copula.BivariateGenerator.exists_diagonal_eq_zero (g : BivariateGenerator) (hg : ¬g.IsStrict) : ∃ (t₀ : ↑unitInterval), t₀ ≠ 0 ∧ ∀ t ≤ t₀, g.cdf t t = 0

The diagonal of a non-strict generator vanishes on an initial interval (0, t₀].

theorem ProbabilityTheory.Copula.BivariateGenerator.isStrict_iff (g : BivariateGenerator) : g.IsStrict ↔ ∀ (u v : ↑unitInterval), u ≠ 0 → v ≠ 0 → 0 < g.cdf u v

A generator is strict iff its copula is positive on (0, 1]².

theorem ProbabilityTheory.Copula.BivariateGenerator.convexOn_invFunReal (g : BivariateGenerator) : ConvexOn ℝ (Set.Ioc 0 1) g.invFunReal

The generator φ is convex on (0, 1] (Nelsen, Section 4.1: the pseudo-inverse of a convex decreasing function is convex).

theorem ProbabilityTheory.Copula.BivariateGenerator.convex_upperLevelSet (g : BivariateGenerator) (t : ↑unitInterval) : Convex ℝ {p : ℝ × ℝ | p ∈ Set.Icc 0 1 ×ˢ Set.Icc 0 1 ∧ ↑t ≤ g.cdf (Set.projIcc 0 1 ⋯ p.1) (Set.projIcc 0 1 ⋯ p.2)}

Nelsen, Theorem 4.3.2 (set form): for every level t, the upper level set {(u, v) ∈ [0,1]² : C(u, v) ≥ t} is convex.

noncomputable def ProbabilityTheory.Copula.BivariateGenerator.levelCurve (g : BivariateGenerator) (t : ↑unitInterval) (x : ℝ) : ℝ

The level curve L_t(u) = ψ(φ(t) − φ(u)) of level t.

Equations

• g.levelCurve t x = g.toFun (g.invFun t - g.invFunReal x)

theorem ProbabilityTheory.Copula.BivariateGenerator.cdf_levelCurve (g : BivariateGenerator) {t u : ↑unitInterval} (ht : t ≠ 0) (htu : t ≤ u) : ∃ (v : ↑unitInterval), ↑v = g.levelCurve t ↑u ∧ g.cdf u v = ↑t

The level curve lies on level t: C(u, L_t(u)) = t for t ≤ u, t > 0.

theorem ProbabilityTheory.Copula.BivariateGenerator.convexOn_levelCurve (g : BivariateGenerator) {t : ↑unitInterval} (ht : t ≠ 0) : ConvexOn ℝ (Set.Icc (↑t) 1) (g.levelCurve t)

Nelsen, Theorem 4.3.2: the level curves of an Archimedean copula are convex.