proposition: Lemma covarianceZl a (X Y : {RV P >-> R}) : P.-integrable setT (EFin \o X) -> P.-integrable setT (EFin \o Y) -> P.-integrable setT (EFin \o (X * Y)%R) -> covariance P (a \o* X)%R Y = a%:E * covariance P X Y.
proof: Proof. move=> X1 Y1 XY1. have aXY : (a \o* X * Y = a \o* (X * Y))%R. by apply/funeqP => x; rewrite mulrAC. rewrite [LHS]covarianceE => [||//|] /=; last 2 first. - by rewrite compre_scale ?integrableZl. - by rewrite aXY compre_scale ?integrableZl. rewrite covarianceE// aXY !expectationM//. by rewrite -muleA -muleBr// fin_num_adde_defr// expectation_fin_num. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly ssrnum ssrint interval finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality) HB(structures) exp numfun lebesgue_measure lebesgue_integral reals ereal signed topology normedtype sequences esum measure exp numfun lebesgue_measure lebesgue_integral