← Copula mathematical handbook

Nelsen's Theorem 4.1.4: an Archimedean formula is a copula iff the generator is convex

Nelsen, An Introduction to Copulas, second edition, Theorem 4.1.4: for a continuous strictly decreasing generator φ : [0, 1] → [0, ∞] with φ(1) = 0 and pseudo-inverse ψ = φ^[-1], the function C(u, v) = ψ(φ(u) + φ(v)) is a copula if and only if φ is convex. The library's BivariateGenerator builds convexity (of ψ on [0, ∞)) into the structure and proves the "if" direction (BivariateGenerator.copula). This file proves the converse.

• ArchimedeanPregenerator: the data of Theorem 4.1.4 without convexity, in the library's inverse-generator convention: ψ ≥ 0 antitone on [0, ∞) and strictly decreasing where it is positive (Nelsen's strictly decreasing φ with pseudo-inverse ψ), and φ a right inverse of ψ on (0, 1] with φ(1) = 0.
• ArchimedeanPregenerator.convexOn_of_copula: if some copula has CDF ψ(φ(u) + φ(v)), then ψ is convex on [0, ∞) (the "only if" of Theorem 4.1.4).
• ArchimedeanPregenerator.exists_copula_iff: Theorem 4.1.4 as an equivalence.
• ArchimedeanPregenerator.toGenerator: the BivariateGenerator of a convex pregenerator.

The proof follows Nelsen: the rectangle inequality on [u₂, u₁] × [v, 1] (Lemma 4.1.3) says ψ(b) + ψ(a + c) ≤ ψ(a) + ψ(b + c) for 0 ≤ a ≤ b, c ≥ 0 (increments of ψ over intervals of a fixed length are nondecreasing, ArchimedeanPregenerator.increment_le). Nelsen then uses midpoint convexity and continuity; we instead use that an antitone function with nondecreasing increments is convex (convexOn_of_antitoneOn_of_increment_le): equal-step increments give the convexity inequality at rational weights, and monotonicity extends it to all weights, so no continuity argument is needed.

theorem ProbabilityTheory.Copula.increment_average_le {f : ℝ → ℝ} (hw : ∀ (a b c : ℝ), 0 ≤ a → a ≤ b → 0 ≤ c → f b + f (a + c) ≤ f a + f (b + c)) {x d : ℝ} (hx : 0 ≤ x) (hd : 0 ≤ d) {m n : ℕ} (hmn : m ≤ n) : ↑n * (f (x + ↑m * d) - f x) ≤ ↑m * (f (x + ↑n * d) - f x)

Equal-step increments: if increments of f over intervals of a fixed length are nondecreasing, then n (f(x + m d) - f(x)) ≤ m (f(x + n d) - f(x)) for m ≤ n.

theorem ProbabilityTheory.Copula.le_of_antitoneOn_of_increment_le {f : ℝ → ℝ} (hanti : AntitoneOn f (Set.Ici 0)) (hw : ∀ (a b c : ℝ), 0 ≤ a → a ≤ b → 0 ≤ c → f b + f (a + c) ≤ f a + f (b + c)) {x y : ℝ} (hx : 0 ≤ x) (hxy : x ≤ y) {b : ℝ} (hb0 : 0 ≤ b) (hb1 : b ≤ 1) : f (x + b * (y - x)) ≤ f x + b * (f y - f x)

The convexity inequality along a segment x ≤ y, from nondecreasing increments and antitonicity.

theorem ProbabilityTheory.Copula.convexOn_of_antitoneOn_of_increment_le {f : ℝ → ℝ} (hanti : AntitoneOn f (Set.Ici 0)) (hw : ∀ (a b c : ℝ), 0 ≤ a → a ≤ b → 0 ≤ c → f b + f (a + c) ≤ f a + f (b + c)) : ConvexOn ℝ (Set.Ici 0) f

An antitone function on [0, ∞) whose increments over intervals of a fixed length are nondecreasing (f(b) + f(a + c) ≤ f(a) + f(b + c) for 0 ≤ a ≤ b, 0 ≤ c) is convex.

structure ProbabilityTheory.Copula.ArchimedeanPregenerator : Type

The data of Nelsen's Theorem 4.1.4 without convexity, in the inverse-generator convention: ψ = toFun is nonnegative and antitone on [0, ∞) and strictly decreasing where positive, and φ = invFun is a right inverse of ψ on (0, 1] with φ(1) = 0.

• toFun : ℝ → ℝ

  Decreasing inverse generator (Nelsen's pseudo-inverse φ^[-1]).

• invFun : ↑unitInterval → ℝ

  Generator on positive unit-interval arguments; its value at zero is unused.

• nonneg (t : ℝ) : 0 ≤ t → 0 ≤ self.toFun t
• antitone : AntitoneOn self.toFun (Set.Ici 0)
• strictAnti (a b : ℝ) : 0 ≤ a → a < b → 0 < self.toFun b → self.toFun b < self.toFun a
• inv_nonneg (u : ↑unitInterval) : u ≠ 0 → 0 ≤ self.invFun u
• inv_one : self.invFun 1 = 0
• right_inv (u : ↑unitInterval) : u ≠ 0 → self.toFun (self.invFun u) = ↑u

noncomputable def ProbabilityTheory.Copula.ArchimedeanPregenerator.cdf (p : ArchimedeanPregenerator) (u v : ↑unitInterval) : ℝ

The Archimedean formula of a pregenerator, with grounded boundary values.

Equations

• p.cdf u v = if u = 0 ∨ v = 0 then 0 else p.toFun (p.invFun u + p.invFun v)

theorem ProbabilityTheory.Copula.ArchimedeanPregenerator.toFun_zero (p : ArchimedeanPregenerator) : p.toFun 0 = 1

theorem ProbabilityTheory.Copula.ArchimedeanPregenerator.toFun_le_one (p : ArchimedeanPregenerator) {s : ℝ} (hs : 0 ≤ s) : p.toFun s ≤ 1

noncomputable def ProbabilityTheory.Copula.ArchimedeanPregenerator.toI (p : ArchimedeanPregenerator) {s : ℝ} (hs : 0 ≤ s) : ↑unitInterval

The value ψ(s) as a point of I.

Equations

• p.toI hs = ⟨p.toFun s, ⋯⟩

theorem ProbabilityTheory.Copula.ArchimedeanPregenerator.toI_ne_zero (p : ArchimedeanPregenerator) {s : ℝ} (hs : 0 ≤ s) (hpos : 0 < p.toFun s) : p.toI hs ≠ 0

theorem ProbabilityTheory.Copula.ArchimedeanPregenerator.invFun_toI (p : ArchimedeanPregenerator) {s : ℝ} (hs : 0 ≤ s) (hpos : 0 < p.toFun s) : p.invFun (p.toI hs) = s

φ(ψ(s)) = s where ψ(s) > 0.

theorem ProbabilityTheory.Copula.ArchimedeanPregenerator.inv_antitone (p : ArchimedeanPregenerator) (u v : ↑unitInterval) (hu : u ≠ 0) (huv : u ≤ v) : p.invFun v ≤ p.invFun u

The generator is antitone on (0, 1] (a consequence of the axioms).

theorem ProbabilityTheory.Copula.ArchimedeanPregenerator.increment_le (p : ArchimedeanPregenerator) (hinc : ∀ (u₁ u₂ v : ↑unitInterval), u₂ ≤ u₁ → 0 ≤ ↑u₁ - ↑u₂ - p.cdf u₁ v + p.cdf u₂ v) {a b c : ℝ} (ha : 0 ≤ a) (hab : a ≤ b) (hc : 0 ≤ c) : p.toFun b + p.toFun (a + c) ≤ p.toFun a + p.toFun (b + c)

The Wright-convexity inequality ψ(b) + ψ(a + c) ≤ ψ(a) + ψ(b + c) (0 ≤ a ≤ b, c ≥ 0) follows from the rectangle inequality on the rectangles [ψ(b), ψ(a)] × [ψ(c), 1].

theorem ProbabilityTheory.Copula.ArchimedeanPregenerator.convexOn_of_rectangle (p : ArchimedeanPregenerator) (hinc : ∀ (u₁ u₂ v : ↑unitInterval), u₂ ≤ u₁ → 0 ≤ ↑u₁ - ↑u₂ - p.cdf u₁ v + p.cdf u₂ v) : ConvexOn ℝ (Set.Ici 0) p.toFun

The "only if" of Nelsen's Theorem 4.1.4, from the rectangle inequality on the rectangles [u₂, u₁] × [v, 1] (Nelsen's Lemma 4.1.3 condition): the inverse generator is convex.

theorem ProbabilityTheory.Copula.ArchimedeanPregenerator.convexOn_of_copula (p : ArchimedeanPregenerator) {C : Copula 2} (hC : ∀ (u v : ↑unitInterval), C.cdf ![u, v] = p.cdf u v) : ConvexOn ℝ (Set.Ici 0) p.toFun

Nelsen, Theorem 4.1.4 ("only if"): if some bivariate copula has the CDF ψ(φ(u) + φ(v)), then the inverse generator ψ is convex on [0, ∞).

noncomputable def ProbabilityTheory.Copula.ArchimedeanPregenerator.toGenerator (p : ArchimedeanPregenerator) (hconv : ConvexOn ℝ (Set.Ici 0) p.toFun) : BivariateGenerator

The BivariateGenerator of a pregenerator with convex inverse generator.

Equations

• p.toGenerator hconv = { toFun := p.toFun, invFun := p.invFun, nonneg := ⋯, antitone := ⋯, convex := hconv, inv_nonneg := ⋯, inv_antitone := ⋯, inv_one := ⋯, right_inv := ⋯ }

@[simp]

theorem ProbabilityTheory.Copula.ArchimedeanPregenerator.toGenerator_cdf (p : ArchimedeanPregenerator) (hconv : ConvexOn ℝ (Set.Ici 0) p.toFun) (u v : ↑unitInterval) : (p.toGenerator hconv).cdf u v = p.cdf u v

theorem ProbabilityTheory.Copula.ArchimedeanPregenerator.exists_copula_iff (p : ArchimedeanPregenerator) : (∃ (C : Copula 2), ∀ (u v : ↑unitInterval), C.cdf ![u, v] = p.cdf u v) ↔ ConvexOn ℝ (Set.Ici 0) p.toFun

Nelsen, Theorem 4.1.4: ψ(φ(u) + φ(v)) is the CDF of a bivariate copula iff the inverse generator ψ is convex on [0, ∞).

noncomputable def ProbabilityTheory.Copula.BivariateGenerator.toPregenerator (g : BivariateGenerator) : ArchimedeanPregenerator

Every bivariate generator is a pregenerator (forgetting convexity).

Equations

• g.toPregenerator = { toFun := g.toFun, invFun := g.invFun, nonneg := ⋯, antitone := ⋯, strictAnti := ⋯, inv_nonneg := ⋯, inv_one := ⋯, right_inv := ⋯ }