proposition: Lemma varianceD_cst_l c (X : {RV P >-> R}) : P.-integrable setT (EFin \o X) -> P.-integrable setT (EFin \o (X ^+ 2)%R) -> 'V_P[(cst c \+ X)%R] = 'V_P[X].
proof: Proof. move=> X1 X2. rewrite varianceD//=; last 3 first. - exact: finite_measure_integrable_cst. - by rewrite compre_scale// integrableZl// finite_measure_integrable_cst. - by rewrite mulrC compre_scale ?integrableZl. by rewrite variance_cst add0e covariance_cst_l mule0 adde0. 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