← Mathematical handbook

Conditional means under copula mixtures

theorem Verification.conditionalMean_mix (C D : ProbabilityTheory.Copula 2) (a : ↑unitInterval) : conditionalMean (C.mix D a) =ᵐ[MeasureTheory.volume] fun (t : ↑unitInterval) => ↑a * conditionalMean C t + (1 - ↑a) * conditionalMean D t

theorem Verification.conditionalMean_independence : conditionalMean (ProbabilityTheory.Copula.independence 2) =ᵐ[MeasureTheory.volume] fun (x : ↑unitInterval) => 1 / 2

theorem Verification.correlationRatio_mix_independence (C : ProbabilityTheory.Copula 2) (a : ↑unitInterval) : correlationRatio (C.mix (ProbabilityTheory.Copula.independence 2) a) = ↑a ^ 2 * correlationRatio C