← Copula mathematical handbook

The converse of McNeil–Nešlehová: d-copula generators are d-monotone

McNeil–Nešlehová (2009), Theorem 2.2 ("only if" part). If C(u) = ψ(φ(u₁) + ⋯ + φ(u_d)) is a d-copula, then the inverse generator ψ is d-monotone on (0, ∞) (HasArchimedeanGenerator.isMultiplyMonotone). Together with the "if" part (MultivariateGenerator.copula) this characterizes the generators of d-dimensional Archimedean copulas (exists_hasArchimedeanGenerator_iff).

The proof has two independent halves.

• From the copula to corner sums. Points ψ(yᵢ) of the unit interval are mapped by the copula to ψ(∑ yᵢ) (HasArchimedeanGenerator.cdf_eq_toFun_sum), so the partial finite differences of C over boxes with corners ψ(yᵢ) and ψ(yᵢ + hᵢ) are the alternating corner sums ∑_{t ⊆ s} (-1)^{|t|} ψ(x + ∑_{i ∈ t} hᵢ). These are probabilities, hence nonnegative, for every x > 0, hᵢ ≥ 0 and |s| ≤ d (HasArchimedeanGenerator.hasNonnegCornerSums).
• From corner sums to d-monotonicity (Williamson 1956; this is the analytic content of the converse). A function with nonnegative corner sums of all orders ≤ n on (0, ∞) is n-monotone (HasNonnegCornerSums.isMultiplyMonotone), by induction on n: orders ≤ 2 give nonnegativity, antitonicity and (through nondecreasing increments, convexOn_of_antitoneOn_of_increment_le) convexity. For n ≥ 3, the difference quotients k_c(x) = (f(x) - f(x + c)) / c have nonnegative corner sums of orders ≤ n - 1, hence are convex; their pointwise limit -f'₊ (minus the right derivative of the convex function f) is therefore convex, hence continuous on (0, ∞), which forces the left and right derivatives of f to agree. So f is differentiable and -f' = lim k_c inherits nonnegative corner sums of orders ≤ n - 1.

No continuity or differentiability of ψ is assumed: it is a consequence.

References: A. J. McNeil and J. Nešlehová, Multivariate Archimedean copulas, d-monotone functions and ℓ₁-norm symmetric distributions, Ann. Statist. 37 (2009) 3059–3097, Theorem 2.2; R. E. Williamson, Multiply monotone functions and their Laplace transforms, Duke Math. J. 23 (1956) 189–207.

Corner sums under reindexing

theorem ProbabilityTheory.Copula.cornerSum_map {ι : Type u_1} {κ : Type u_2} (e : ι ↪ κ) (f : ℝ → ℝ) (x : ℝ) (h : κ → ℝ) (s : Finset ι) : cornerSum f x h (Finset.map e s) = cornerSum f x (h ∘ ⇑e) s

theorem ProbabilityTheory.Copula.cornerSum_fin_cons {k : ℕ} (f : ℝ → ℝ) (x c : ℝ) (h : Fin k → ℝ) : cornerSum f x (Fin.cons c h) Finset.univ = cornerSum f x h Finset.univ - cornerSum f (x + c) h Finset.univ

Adding a coordinate in front: Δ_{(c, h)} f (x) = Δ_h f (x) - Δ_h f (x + c).

theorem ProbabilityTheory.Copula.cornerSum_diffQuot {ι : Type u_1} (f : ℝ → ℝ) (x c : ℝ) (h : ι → ℝ) (s : Finset ι) : cornerSum (fun (y : ℝ) => (f y - f (y + c)) / c) x h s = (cornerSum f x h s - cornerSum f (x + c) h s) / c

Corner sums of the difference quotient (f(x) - f(x + c)) / c.

Functions with nonnegative corner sums

def ProbabilityTheory.Copula.HasNonnegCornerSums (n : ℕ) (f : ℝ → ℝ) : Prop

f has nonnegative alternating corner sums of all orders ≤ n on (0, ∞): ∑_{t ⊆ {1,…,k}} (-1)^{|t|} f(x + ∑_{i ∈ t} hᵢ) ≥ 0 for k ≤ n, x > 0, hᵢ ≥ 0.

Equations

• ProbabilityTheory.Copula.HasNonnegCornerSums n f = ∀ k ≤ n, ∀ (x : ℝ), 0 < x → ∀ (h : Fin k → ℝ), (∀ (i : Fin k), 0 ≤ h i) → 0 ≤ ProbabilityTheory.Copula.cornerSum f x h Finset.univ

theorem ProbabilityTheory.Copula.HasNonnegCornerSums.mono {n : ℕ} {f : ℝ → ℝ} {m : ℕ} (hf : HasNonnegCornerSums n f) (hmn : m ≤ n) : HasNonnegCornerSums m f

theorem ProbabilityTheory.Copula.HasNonnegCornerSums.nonneg {n : ℕ} {f : ℝ → ℝ} (hf : HasNonnegCornerSums n f) {x : ℝ} (hx : 0 < x) : 0 ≤ f x

theorem ProbabilityTheory.Copula.HasNonnegCornerSums.antitoneOn {n : ℕ} {f : ℝ → ℝ} (hf : HasNonnegCornerSums n f) (hn : 1 ≤ n) : AntitoneOn f (Set.Ioi 0)

theorem ProbabilityTheory.Copula.HasNonnegCornerSums.corner_two {n : ℕ} {f : ℝ → ℝ} (hf : HasNonnegCornerSums n f) (hn : 2 ≤ n) {x a b : ℝ} (hx : 0 < x) (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ f x - f (x + b) - f (x + a) + f (x + a + b)

theorem ProbabilityTheory.Copula.HasNonnegCornerSums.convexOn {n : ℕ} {f : ℝ → ℝ} (hf : HasNonnegCornerSums n f) (hn : 2 ≤ n) : ConvexOn ℝ (Set.Ioi 0) f

theorem ProbabilityTheory.Copula.HasNonnegCornerSums.diffQuot {n : ℕ} {f : ℝ → ℝ} (hf : HasNonnegCornerSums (n + 1) f) {c : ℝ} (hc : 0 < c) : HasNonnegCornerSums n fun (y : ℝ) => (f y - f (y + c)) / c

The difference quotients (f(x) - f(x + c)) / c, c > 0, have nonnegative corner sums of one order less.

theorem ProbabilityTheory.Copula.HasNonnegCornerSums.tendsto_diffQuot {n : ℕ} {f : ℝ → ℝ} (hf : HasNonnegCornerSums n f) (hn : 2 ≤ n) {x : ℝ} (hx : 0 < x) : Filter.Tendsto (fun (c : ℝ) => (f x - f (x + c)) / c) (nhdsWithin 0 (Set.Ioi 0)) (nhds (-derivWithin f (Set.Ioi x) x))

The difference quotients converge to minus the right derivative.

theorem ProbabilityTheory.Copula.HasNonnegCornerSums.convexOn_neg_rightDeriv {n : ℕ} {f : ℝ → ℝ} (hf : HasNonnegCornerSums (n + 3) f) : ConvexOn ℝ (Set.Ioi 0) fun (x : ℝ) => -derivWithin f (Set.Ioi x) x

For n ≥ 3, minus the right derivative is convex on (0, ∞).

theorem ProbabilityTheory.Copula.HasNonnegCornerSums.hasDerivAt {n : ℕ} {f : ℝ → ℝ} (hf : HasNonnegCornerSums (n + 3) f) {x : ℝ} (hx : 0 < x) : HasDerivAt f (derivWithin f (Set.Ioi x) x) x

For n ≥ 3, f is differentiable on (0, ∞): the right derivative is continuous, so it agrees with the left derivative.

theorem ProbabilityTheory.Copula.HasNonnegCornerSums.differentiableOn {n : ℕ} {f : ℝ → ℝ} (hf : HasNonnegCornerSums (n + 3) f) : DifferentiableOn ℝ f (Set.Ioi 0)

theorem ProbabilityTheory.Copula.HasNonnegCornerSums.neg_deriv {n : ℕ} {f : ℝ → ℝ} (hf : HasNonnegCornerSums (n + 3) f) : HasNonnegCornerSums (n + 2) fun (x : ℝ) => -deriv f x

For n ≥ 3, -f' has nonnegative corner sums of orders ≤ n - 1.

theorem ProbabilityTheory.Copula.HasNonnegCornerSums.isMultiplyMonotone {n : ℕ} {f : ℝ → ℝ} : HasNonnegCornerSums n f → IsMultiplyMonotone n f

Williamson's characterization: nonnegative corner sums of all orders ≤ n on (0, ∞) imply n-monotonicity.

theorem ProbabilityTheory.Copula.isMultiplyMonotone_iff_hasNonnegCornerSums {n : ℕ} {f : ℝ → ℝ} : IsMultiplyMonotone n f ↔ HasNonnegCornerSums n f

n-monotone functions are exactly the functions with nonnegative alternating corner sums of all orders ≤ n on (0, ∞) (Williamson 1956; McNeil–Nešlehová 2009).

From the copula to corner sums

theorem ProbabilityTheory.Copula.BivariateGenerator.continuousWithinAt_toFun_zero (g : BivariateGenerator) : ContinuousWithinAt g.toFun (Set.Ici 0) 0

The inverse generator is right-continuous at 0: it takes every value of (0,1].

theorem ProbabilityTheory.Copula.BivariateGenerator.continuousOn_toFun (g : BivariateGenerator) : ContinuousOn g.toFun (Set.Ici 0)

The inverse generator of a bivariate generator is continuous on [0, ∞).

theorem ProbabilityTheory.Copula.HasArchimedeanGenerator.cdf_toI {d : ℕ} {C : Copula d} {g : BivariateGenerator} (hC : C.HasArchimedeanGenerator g) (y : Fin d → ℝ) (hy : ∀ (i : Fin d), 0 ≤ y i) : (C.cdf fun (i : Fin d) => g.toI ⋯) = g.toFun (∑ i : Fin d, y i)

An Archimedean copula maps the point (ψ(y₁), …, ψ(y_d)) to ψ(y₁ + ⋯ + y_d), for all yᵢ ≥ 0 (including the case where some ψ(yᵢ) = 0).

theorem ProbabilityTheory.Copula.HasArchimedeanGenerator.hasNonnegCornerSums {d : ℕ} {C : Copula d} {g : BivariateGenerator} (hC : C.HasArchimedeanGenerator g) : HasNonnegCornerSums d g.toFun

The generator of a d-dimensional Archimedean copula has nonnegative corner sums of all orders ≤ d.

theorem ProbabilityTheory.Copula.HasArchimedeanGenerator.isMultiplyMonotone {d : ℕ} {C : Copula d} {g : BivariateGenerator} (hC : C.HasArchimedeanGenerator g) : IsMultiplyMonotone d g.toFun

McNeil–Nešlehová (2009), Theorem 2.2, "only if": the inverse generator of a d-dimensional Archimedean copula is d-monotone on (0, ∞).

theorem ProbabilityTheory.Copula.exists_hasArchimedeanGenerator_iff {d : ℕ} (g : BivariateGenerator) : (∃ (C : Copula d), C.HasArchimedeanGenerator g) ↔ IsMultiplyMonotone d g.toFun

McNeil–Nešlehová (2009), Theorem 2.2: a bivariate Archimedean generator generates a d-dimensional copula ψ(φ(u₁) + ⋯ + φ(u_d)) if and only if ψ is d-monotone.