proposition: Lemma covarianceNl (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 (\- X)%R Y = - covariance P X Y.
proof: Proof. move=> X1 Y1 XY1. have -> : (\- X = -1 \o* X)%R by apply/funeqP => x /=; rewrite mulrN mulr1. by rewrite covarianceZl// EFinN mulNe mul1e. 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