Margins of `d`-copulas and the independence copula #

For a d-copula C and a coordinate map ρ : Fin e → Fin d, C.reindex ρ is the law of (X_{ρ 0}, …, X_{ρ (e-1)}). When ρ is injective this is the e-dimensional margin of C (Nelsen 2006, §2.10: the k-margins of a d-copula are k-copulas, obtained by setting the remaining arguments equal to 1). This module proves

the CDF of any reindexed copula, C.reindex ρ at v, is C at the point marginPoint ρ v whose i-th coordinate is the minimum of the v j with ρ j = i (and 1 if there is none) (cdf_reindex); for injective ρ this is "set the other arguments to 1" (cdf_reindex_of_injective);
margins of Π_d are Π_e (reindex_independence), margins (and repetitions) of M_d are M_e (reindex_comonotonic), and margins commute with reflections (reindex_reflect), in particular with survival copulas (reindex_survivalCopula);
the characterization of the independence copula: C = Π_d iff the coordinates are mutually independent under C (eq_independence_iff_iIndepFun) iff C(u) = ∏ uᵢ (eq_independence_iff_cdf) (Nelsen 2006, §2.10, in copula form).

source

noncomputable def ProbabilityTheory.Copula.marginPoint {d e : ℕ} (ρ : Fin e → Fin d) (v : Fin e → ↑unitInterval) (i : Fin d) :

↑unitInterval

The point of [0,1]^d at which a d-copula is evaluated to obtain the CDF of C.reindex ρ at v: coordinate i is the minimum of the v j with ρ j = i, and 1 if there is none.

Equations

ProbabilityTheory.Copula.marginPoint ρ v i = ⨅ (j : Fin e), ⨅ (_ : ρ j = i), v j

Instances For

source

theorem ProbabilityTheory.Copula.le_marginPoint_iff {d e : ℕ} (ρ : Fin e → Fin d) (v : Fin e → ↑unitInterval) (x : Fin d → ↑unitInterval) :

x ≤ marginPoint ρ v ↔ ∀ (j : Fin e), x (ρ j) ≤ v j

source

theorem ProbabilityTheory.Copula.marginPoint_apply_of_injective {d e : ℕ} {ρ : Fin e → Fin d} (hρ : Function.Injective ρ) (v : Fin e → ↑unitInterval) (j : Fin e) :

marginPoint ρ v (ρ j) = v j

source

theorem ProbabilityTheory.Copula.marginPoint_apply_of_notMem_range {d e : ℕ} (ρ : Fin e → Fin d) (v : Fin e → ↑unitInterval) {i : Fin d} (hi : i ∉ Set.range ρ) :

marginPoint ρ v i = 1

source

theorem ProbabilityTheory.Copula.cdf_reindex {d e : ℕ} (C : Copula d) (ρ : Fin e → Fin d) (v : Fin e → ↑unitInterval) :

(C.reindex ρ).cdf v = C.cdf (marginPoint ρ v)

CDF of a reindexed copula: evaluate C at marginPoint ρ v.

source

theorem ProbabilityTheory.Copula.cdf_reindex_of_injective {d e : ℕ} (C : Copula d) {ρ : Fin e → Fin d} (hρ : Function.Injective ρ) (v : Fin e → ↑unitInterval) (x : Fin d → ↑unitInterval) (hx : ∀ (j : Fin e), x (ρ j) = v j) (h1 : ∀ i ∉ Set.range ρ, x i = 1) :

(C.reindex ρ).cdf v = C.cdf x

Margins of a d-copula (Nelsen 2006, §2.10): for injective ρ, the CDF of the margin C.reindex ρ is obtained by putting v j in coordinate ρ j and 1 elsewhere.

source

theorem ProbabilityTheory.Copula.cdf_reindex_pair {d : ℕ} (C : Copula d) {i j : Fin d} (hij : i ≠ j) (s t : ↑unitInterval) :

(C.reindex ![i, j]).cdf ![s, t] = C.cdf (Function.update (Function.update (fun (x : Fin d) => 1) i s) j t)

Bivariate margins: the (i, j) margin evaluated at (s, t).

source

theorem ProbabilityTheory.Copula.reindex_independence {d e : ℕ} {ρ : Fin e → Fin d} (hρ : Function.Injective ρ) :

(independence d).reindex ρ = independence e

Margins of the independence copula are independence copulas.

source

theorem ProbabilityTheory.Copula.reindex_comonotonic {d e : ℕ} (ρ : Fin e → Fin d) :

(comonotonic d).reindex ρ = comonotonic e

Margins and repetitions of the comonotonic copula are comonotonic.

source

theorem ProbabilityTheory.Copula.reindex_reflect {d e : ℕ} (C : Copula d) (s : Finset (Fin d)) (ρ : Fin e → Fin d) :

(C.reflect s).reindex ρ = (C.reindex ρ).reflect {j : Fin e | ρ j ∈ s}

Margins commute with reflections: reflecting the coordinates in s and then taking the ρ-margin is the same as taking the margin and reflecting the coordinates mapped into s.

source