Survival functions, survival copulas and reflections in dimension `d` #

For a d-copula C with law P of U = (U₁, …, U_d) (Nelsen 2006, §2.10 and the end of §2.6; Durante–Sempi 2016, §1.7.2):

the survival function C̄(u) = P(U ≥ u) is the C-volume of the box [u, 1], i.e. the inclusion–exclusion sum ∑_{S} (-1)^{|S|} C(u_S, 1) over the coordinate sets S (survival_eq_rectangleIncrement, survival_eq_sum_powerset);
the survival copula Ĉ (the law of 1 - U) satisfies Ĉ(u) = C̄(1 - u) (cdf_survivalCopula_eq_survival), hence Ĉ(u) = ∑_{S} (-1)^{|S|} C((1 - u)_S, 1) (cdf_survivalCopula_eq_sum);
more generally, reflecting the coordinates in s gives the copula of (1 - Uᵢ)_{i ∈ s}, (Uᵢ)_{i ∉ s} whose CDF is a partial finite difference of C (cdf_reflect);
Π_d and M_d are radially symmetric (survivalCopula_independence, survivalCopula_comonotonic).

source

theorem ProbabilityTheory.Copula.partialIncrement_cdf_eq {d : ℕ} (C : Copula d) (a b : Fin d → ↑unitInterval) (s : Finset (Fin d)) (hab : a ≤ b) :

partialIncrement C.cdf a b s = C.toMeasure.real {x : Fin d → ↑unitInterval | x ≤ b ∧ ∀ i ∈ s, a i < x i}

Former name of partialIncrement_cdf (now public in Copula.Rectangle).

source

theorem ProbabilityTheory.Copula.survival_eq_rectangleIncrement {d : ℕ} (C : Copula d) (u : Fin d → ↑unitInterval) :

C.survival u = rectangleIncrement C.cdf u fun (x : Fin d) => 1

The survival function is the C-volume of [u, 1].

source

theorem ProbabilityTheory.Copula.survival_eq_sum_powerset {d : ℕ} (C : Copula d) (u : Fin d → ↑unitInterval) :

C.survival u = ∑ t ∈ Finset.univ.powerset, (-1) ^ t.card * C.cdf (corner u (fun (x : Fin d) => 1) t)

Inclusion–exclusion for the survival function (Nelsen 2006, §2.10): C̄(u) = ∑_{S ⊆ {1,…,d}} (-1)^{|S|} C(v^S) with v^S_i = uᵢ for i ∈ S and 1 otherwise.

source

theorem ProbabilityTheory.Copula.cdf_reflect {d : ℕ} (C : Copula d) (s : Finset (Fin d)) (u : Fin d → ↑unitInterval) :

(C.reflect s).cdf u = partialIncrement C.cdf (reflectPoint s u) (fun (i : Fin d) => if i ∈ s then 1 else u i) s

CDF of a reflected copula. Reflecting the coordinates in s gives the partial finite difference of C over s between 1 - uᵢ and 1, with the other coordinates held at uᵢ.

source