← Copula mathematical handbook

Probability laws and integration for copula mixtures

theorem ProbabilityTheory.Copula.toMeasure_mix {d : ℕ} (C D : Copula d) (a : ↑unitInterval) : (C.mix D a).toMeasure = ENNReal.ofReal ↑a • C.toMeasure + ENNReal.ofReal (1 - ↑a) • D.toMeasure

theorem ProbabilityTheory.Copula.integral_mix {d : ℕ} (C D : Copula d) (a : ↑unitInterval) {f : (Fin d → ↑unitInterval) → ℝ} (hf : Continuous f) : ∫ (x : Fin d → ↑unitInterval), f x ∂(C.mix D a).toMeasure = ↑a * ∫ (x : Fin d → ↑unitInterval), f x ∂C.toMeasure + (1 - ↑a) * ∫ (x : Fin d → ↑unitInterval), f x ∂D.toMeasure

Integrating against a mixture averages the two integrals with the same weights.