← Copula mathematical handbook

Finite mixtures of copulas

theorem ProbabilityTheory.Copula.rectangleIncrement_sum {d n : ℕ} (F : Fin n → (Fin d → ↑unitInterval) → ℝ) (w : Fin n → ℝ) (a b : Fin d → ↑unitInterval) : rectangleIncrement (fun (u : Fin d → ↑unitInterval) => ∑ j : Fin n, w j * F j u) a b = ∑ j : Fin n, w j * rectangleIncrement (F j) a b

theorem ProbabilityTheory.Copula.isClassical_mixture {d n : ℕ} (C : Fin n → Copula d) (w : Fin n → ℝ) (hw : ∀ (j : Fin n), 0 ≤ w j) (hsum : ∑ j : Fin n, w j = 1) : IsClassical fun (u : Fin d → ↑unitInterval) => ∑ j : Fin n, w j * (C j).cdf u

Nonnegative finite mixtures preserve all classical copula conditions.

noncomputable def ProbabilityTheory.Copula.finiteMixture {d n : ℕ} (C : Fin n → Copula d) (w : Fin n → ℝ) (hw : ∀ (j : Fin n), 0 ≤ w j) (hsum : ∑ j : Fin n, w j = 1) : Copula d

A finite mixture with real nonnegative weights summing to one.

Equations

• ProbabilityTheory.Copula.finiteMixture C w hw hsum = ProbabilityTheory.Copula.ofClassical (fun (u : Fin d → ↑unitInterval) => ∑ j : Fin n, w j * (C j).cdf u) ⋯

@[simp]

theorem ProbabilityTheory.Copula.cdf_finiteMixture {d n : ℕ} (C : Fin n → Copula d) (w : Fin n → ℝ) (hw : ∀ (j : Fin n), 0 ≤ w j) (hsum : ∑ j : Fin n, w j = 1) (u : Fin d → ↑unitInterval) : (finiteMixture C w hw hsum).cdf u = ∑ j : Fin n, w j * (C j).cdf u

noncomputable def ProbabilityTheory.Copula.mix {d : ℕ} (C D : Copula d) (a : ↑unitInterval) : Copula d

A two-component convex mixture. The first copula has weight a.

Equations

• C.mix D a = ProbabilityTheory.Copula.finiteMixture ![C, D] ![↑a, 1 - ↑a] ⋯ ⋯

@[simp]

theorem ProbabilityTheory.Copula.cdf_mix {d : ℕ} (C D : Copula d) (a : ↑unitInterval) (u : Fin d → ↑unitInterval) : (C.mix D a).cdf u = ↑a * C.cdf u + (1 - ↑a) * D.cdf u

@[simp]

theorem ProbabilityTheory.Copula.mix_zero {d : ℕ} (C D : Copula d) : C.mix D 0 = D

@[simp]

theorem ProbabilityTheory.Copula.mix_one {d : ℕ} (C D : Copula d) : C.mix D 1 = C