← Copula mathematical handbook

d-monotone functions and alternating corner sums

McNeil and Nešlehová (2009, Definition 2.3) call a real function ψ on (0, ∞) d-monotone (d ≥ 2) if it is differentiable up to order d - 2, the derivatives satisfy (-1)^k ψ^{(k)} ≥ 0 for k ≤ d - 2, and (-1)^{d-2} ψ^{(d-2)} is nonincreasing and convex; 1-monotone means nonnegative and nonincreasing. We encode this recursively (IsMultiplyMonotone): a function is (n+3)-monotone if it is nonnegative and differentiable on (0, ∞) and -ψ' is (n+2)-monotone.

The analytic heart of the Archimedean construction in dimension d is the sign of the alternating corner sums cornerSum ψ x h s = ∑_{t ⊆ s} (-1)^{|t|} ψ(x + ∑_{i ∈ t} hᵢ), which are exactly the rectangle increments of u ↦ ψ(∑ φ(uᵢ)). We prove (IsMultiplyMonotone.cornerSum_nonneg) that a d-monotone ψ has nonnegative corner sums for all s with |s| ≤ d, all x > 0 and all hᵢ ≥ 0 (the "if" direction of McNeil–Nešlehová 2009, Theorem 2.2, in its analytic form; Williamson 1956), and extend this to x = 0 for continuous ψ (IsMultiplyMonotone.cornerSum_nonneg_of_nonneg). The proof is by induction on d via the mean value theorem; the base case d = 2 is the convexity of ψ. Completely monotone functions (Kimberling 1974) are d-monotone for every d.

Power functions c (1 + t)^{-α} with c ≥ 0, α > 0 are d-monotone for every d (isMultiplyMonotone_one_add_rpow_neg); they generate the Clayton family.

Alternating corner sums

noncomputable def ProbabilityTheory.Copula.cornerSum {ι : Type u_1} (f : ℝ → ℝ) (x : ℝ) (h : ι → ℝ) (s : Finset ι) : ℝ

The alternating corner sum ∑_{t ⊆ s} (-1)^{|t|} f(x + ∑_{i ∈ t} hᵢ), i.e. the iterated difference (-Δ_{h_{i₁}}) ⋯ (-Δ_{h_{iₖ}}) f (x) over the coordinates of s.

Equations

• ProbabilityTheory.Copula.cornerSum f x h s = ∑ t ∈ s.powerset, (-1) ^ t.card * f (x + ∑ i ∈ t, h i)

@[simp]

theorem ProbabilityTheory.Copula.cornerSum_empty {ι : Type u_1} (f : ℝ → ℝ) (x : ℝ) (h : ι → ℝ) : cornerSum f x h ∅ = f x

theorem ProbabilityTheory.Copula.cornerSum_insert {ι : Type u_1} [DecidableEq ι] (f : ℝ → ℝ) (x : ℝ) (h : ι → ℝ) {s : Finset ι} {j : ι} (hj : j ∉ s) : cornerSum f x h (insert j s) = cornerSum f x h s - cornerSum f (x + h j) h s

The recursion cornerSum f x h (insert j s) = A(x) - A(x + hⱼ) with A = cornerSum f · h s.

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

theorem ProbabilityTheory.Copula.cornerSum_singleton {ι : Type u_1} (f : ℝ → ℝ) (x : ℝ) (h : ι → ℝ) (j : ι) : cornerSum f x h {j} = f x - f (x + h j)

theorem ProbabilityTheory.Copula.cornerSum_pair {ι : Type u_1} [DecidableEq ι] (f : ℝ → ℝ) (x : ℝ) (h : ι → ℝ) {j k : ι} (hjk : j ≠ k) : cornerSum f x h {j, k} = f x - f (x + h k) - f (x + h j) + f (x + h j + h k)

theorem ProbabilityTheory.Copula.hasDerivAt_cornerSum {ι : Type u_1} {f f' : ℝ → ℝ} {x : ℝ} {h : ι → ℝ} {s : Finset ι} (hf : ∀ t ∈ s.powerset, HasDerivAt f (f' (x + ∑ i ∈ t, h i)) (x + ∑ i ∈ t, h i)) : HasDerivAt (fun (y : ℝ) => cornerSum f y h s) (cornerSum f' x h s) x

Corner sums are differentiable in the base point, with the corner sum of the derivative.

theorem ProbabilityTheory.Copula.cornerSum_congr {ι : Type u_1} {f g : ℝ → ℝ} {x : ℝ} {h : ι → ℝ} {s : Finset ι} (hfg : ∀ t ∈ s.powerset, f (x + ∑ i ∈ t, h i) = g (x + ∑ i ∈ t, h i)) : cornerSum f x h s = cornerSum g x h s

Corner sums depend only on the values of f on the corners.

theorem ProbabilityTheory.Copula.add_sum_nonneg {ι : Type u_1} {x : ℝ} {h : ι → ℝ} {s : Finset ι} (hx : 0 ≤ x) (hh : ∀ i ∈ s, 0 ≤ h i) {t : Finset ι} (ht : t ∈ s.powerset) : 0 ≤ x + ∑ i ∈ t, h i

theorem ProbabilityTheory.Copula.add_sum_pos {ι : Type u_1} {x : ℝ} {h : ι → ℝ} {s : Finset ι} (hx : 0 < x) (hh : ∀ i ∈ s, 0 ≤ h i) {t : Finset ι} (ht : t ∈ s.powerset) : 0 < x + ∑ i ∈ t, h i

d-monotone functions

def ProbabilityTheory.Copula.IsMultiplyMonotone : ℕ → (ℝ → ℝ) → Prop

d-monotone functions on (0, ∞) (McNeil–Nešlehová 2009, Definition 2.3), defined recursively: 0-monotone means nonnegative, 1-monotone nonnegative and nonincreasing, 2-monotone nonnegative, nonincreasing and convex, and (n+3)-monotone means nonnegative, differentiable, with -ψ' being (n+2)-monotone.

Equations

• One or more equations did not get rendered due to their size.
• ProbabilityTheory.Copula.IsMultiplyMonotone 0 x✝ = ∀ (x : ℝ), 0 < x → 0 ≤ x✝ x
• ProbabilityTheory.Copula.IsMultiplyMonotone 1 x✝ = ((∀ (x : ℝ), 0 < x → 0 ≤ x✝ x) ∧ AntitoneOn x✝ (Set.Ioi 0))
• ProbabilityTheory.Copula.IsMultiplyMonotone 2 x✝ = ((∀ (x : ℝ), 0 < x → 0 ≤ x✝ x) ∧ AntitoneOn x✝ (Set.Ioi 0) ∧ ConvexOn ℝ (Set.Ioi 0) x✝)

theorem ProbabilityTheory.Copula.IsMultiplyMonotone.nonneg {n : ℕ} {f : ℝ → ℝ} : IsMultiplyMonotone n f → ∀ (x : ℝ), 0 < x → 0 ≤ f x

theorem ProbabilityTheory.Copula.IsMultiplyMonotone.congr {n : ℕ} {f g : ℝ → ℝ} : IsMultiplyMonotone n f → Set.EqOn f g (Set.Ioi 0) → IsMultiplyMonotone n g

d-monotonicity depends only on the values on (0, ∞).

theorem ProbabilityTheory.Copula.IsMultiplyMonotone.const_mul {n : ℕ} {f : ℝ → ℝ} : IsMultiplyMonotone n f → ∀ {c : ℝ}, 0 ≤ c → IsMultiplyMonotone n fun (x : ℝ) => c * f x

Nonnegative multiples of d-monotone functions are d-monotone.

theorem ProbabilityTheory.Copula.IsMultiplyMonotone.antitoneOn {n : ℕ} {f : ℝ → ℝ} : IsMultiplyMonotone (n + 1) f → AntitoneOn f (Set.Ioi 0)

A d-monotone function is nonincreasing on (0, ∞) for d ≥ 1.

theorem ProbabilityTheory.Copula.IsMultiplyMonotone.cornerSum_nonneg {ι : Type u_1} [DecidableEq ι] {n : ℕ} {f : ℝ → ℝ} : IsMultiplyMonotone n f → ∀ {h : ι → ℝ} {s : Finset ι}, s.card ≤ n → ∀ {x : ℝ}, 0 < x → (∀ i ∈ s, 0 ≤ h i) → 0 ≤ cornerSum f x h s

Corner sums of d-monotone functions are nonnegative (McNeil–Nešlehová 2009, Theorem 2.2, analytic part; Williamson 1956): for |s| ≤ d, x > 0 and hᵢ ≥ 0, ∑_{t ⊆ s} (-1)^{|t|} ψ(x + ∑_{i ∈ t} hᵢ) ≥ 0.

theorem ProbabilityTheory.Copula.IsMultiplyMonotone.cornerSum_nonneg_of_nonneg {ι : Type u_1} [DecidableEq ι] {n : ℕ} {f : ℝ → ℝ} (hf : IsMultiplyMonotone n f) (hc : ContinuousOn f (Set.Ici 0)) {h : ι → ℝ} {s : Finset ι} (hs : s.card ≤ n) {x : ℝ} (hx : 0 ≤ x) (hh : ∀ i ∈ s, 0 ≤ h i) : 0 ≤ cornerSum f x h s

Corner sums at the boundary point x = 0, for ψ continuous on [0, ∞).

Power functions

theorem ProbabilityTheory.Copula.isMultiplyMonotone_one_add_rpow_neg (n : ℕ) {c α : ℝ} : 0 ≤ c → 0 < α → IsMultiplyMonotone n fun (t : ℝ) => c * (1 + t) ^ (-α)

c (1 + t)^{-α} is d-monotone for every d (c ≥ 0, α > 0); these functions are completely monotone and generate the Clayton family.