proposition: Lemma covarianceNN (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)%R = covariance P X Y.
proof: Proof. move=> X1 Y1 XY1. have NY : P.-integrable setT (EFin \o (\- Y)%R) by rewrite compreN ?integrableN. by rewrite covarianceNl ?covarianceNr ?oppeK//= mulrN compreN ?integrableN. 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