Conditional CDFs of mixtures #
Uniform first marginals make the conditional mixture weights constant. All identities are almost everywhere in the conditioning coordinate, for each threshold separately, and include singular copulas and zero weights.
theorem
ProbabilityTheory.Copula.conditionalCDF_finiteMixture
{n : ℕ}
(C : Fin n → Copula 2)
(w : Fin n → ℝ)
(hw : ∀ (j : Fin n), 0 ≤ w j)
(hsum : ∑ j : Fin n, w j = 1)
(v : ↑unitInterval)
:
(fun (u : ↑unitInterval) => (finiteMixture C w hw hsum).conditionalCDF u v) =ᵐ[MeasureTheory.volume]
fun (u : ↑unitInterval) => ∑ j : Fin n, w j * (C j).conditionalCDF u v
theorem
ProbabilityTheory.Copula.conditionalCDF_mix
(C D : Copula 2)
(a v : ↑unitInterval)
:
(fun (u : ↑unitInterval) => (C.mix D a).conditionalCDF u v) =ᵐ[MeasureTheory.volume] fun (u : ↑unitInterval) =>
↑a * C.conditionalCDF u v + (1 - ↑a) * D.conditionalCDF u v
theorem
ProbabilityTheory.Copula.conditionalCDF_independence
(v : ↑unitInterval)
:
(fun (u : ↑unitInterval) => (independence 2).conditionalCDF u v) =ᵐ[MeasureTheory.volume] fun (x : ↑unitInterval) => ↑v