theorem
ProbabilityTheory.Copula.RankRegion.integral_ordinalSum_measurable
(C D : Copula 2)
(a : ↑unitInterval)
{f : (Fin 2 → ↑unitInterval) → ℝ}
(hf : Measurable f)
(hL :
MeasureTheory.Integrable (fun (x : Fin 2 → ↑unitInterval) => f fun (i : Fin 2) => OrdinalSum.lowerEmbed a (x i))
C.toMeasure)
(hU :
MeasureTheory.Integrable (fun (x : Fin 2 → ↑unitInterval) => f fun (i : Fin 2) => OrdinalSum.upperEmbed a (x i))
D.toMeasure)
:
∫ (x : Fin 2 → ↑unitInterval), f x ∂(C.ordinalSum D a).toMeasure = ↑a * ∫ (x : Fin 2 → ↑unitInterval), f fun (i : Fin 2) => OrdinalSum.lowerEmbed a (x i) ∂C.toMeasure + (1 - ↑a) * ∫ (x : Fin 2 → ↑unitInterval), f fun (i : Fin 2) => OrdinalSum.upperEmbed a (x i) ∂D.toMeasure
Integrate a measurable observable when its two pullbacks are integrable. This includes the threshold signs in magnitude constructions.