proposition: Lemma varianceZ a (X : {RV P >-> R}) : P.-integrable setT (EFin \o X) -> P.-integrable setT (EFin \o (X ^+ 2)%R) -> 'V_P[(a \o* X)%R] = (a ^+ 2)%:E * 'V_P[X].
proof: Proof. move=> X1 X2; rewrite /variance covarianceZl//=. - by rewrite covarianceZr// muleA. - by rewrite compre_scale// integrableZl. - rewrite [X in EFin \o X](_ : _ = (a \o* X ^+ 2)%R); last first. by apply/funeqP => x; rewrite mulrA. by rewrite compre_scale// integrableZl. 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