proposition: Lemma covarianceE (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 Y = 'E_P[X * Y] - 'E_P[X] * 'E_P[Y].
proof: Proof. move=> X1 Y1 XY1. have ? : 'E_P[X] \is a fin_num by rewrite fin_num_abs// integrable_expectation. have ? : 'E_P[Y] \is a fin_num by rewrite fin_num_abs// integrable_expectation. rewrite unlock [X in 'E_P[X]](_ : _ = (X \* Y \- fine 'E_P[X] \o* Y \- fine 'E_P[Y] \o* X \+ fine ('E_P[X] * 'E_P[Y]) \o* cst 1)%R); last first. apply/funeqP => x /=; rewrite mulrDr !mulrDl/= mul1r fineM// mulrNN addrA. by rewrite mulrN mulNr [Z in (X x * Y x - Z)%R]mulrC. have ? : P.-integrable [set: T] (EFin \o (X \* Y \- fine 'E_P[X] \o* Y)%R). by rewrite compreBr ?integrableB// compre_scale ?integrableZl. rewrite expectationD/=; last 2 first. - by rewrite compreBr// integrableB// compre_scale ?integrableZl. - by rewrite compre_scale// integrableZl// finite_measure_integrable_cst. rewrite 2?expectationB//= ?compre_scale// ?integrableZl//. rewrite 3?expectationM//= ?finite_measure_integrable_cst//. by rewrite expectation_cst mule1 fineM// EFinM !fineK// muleC subeK ?fin_numM. 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