proposition: Lemma covariance_le (X Y : {RV P >-> R}) : P.-integrable setT (EFin \o X) -> P.-integrable setT (EFin \o (X ^+ 2)%R) -> P.-integrable setT (EFin \o Y) -> P.-integrable setT (EFin \o (Y ^+ 2)%R) -> P.-integrable setT (EFin \o (X * Y)%R) -> covariance P X Y <= sqrte 'V_P[X] * sqrte 'V_P[Y].
proof: Proof. move=> X1 X2 Y1 Y2 XY1. rewrite -sqrteM ?variance_ge0//. rewrite lee_sqrE ?sqrte_ge0// sqr_sqrte ?mule_ge0 ?variance_ge0//. rewrite -(fineK (variance_fin_num X1 X2)) -(fineK (variance_fin_num Y1 Y2)). rewrite -(fineK (covariance_fin_num X1 Y1 XY1)). rewrite -EFin_expe -EFinM lee_fin -(@ler_pM2l _ 4) ?ltr0n// [leRHS]mulrA. rewrite [in leLHS](_ : 4 = 2 * 2)%R -natrM// [in leLHS]natrM mulrACA -expr2. rewrite -subr_le0; apply: deg_le2_ge0 => r; rewrite -lee_fin !EFinD. rewrite EFinM fineK ?variance_fin_num// muleC -varianceZ//. rewrite 2!EFinM ?fineK ?variance_fin_num// ?covariance_fin_num//. rewrite -muleA [_ * r%:E]muleC -covarianceZl//. rewrite addeAC -varianceD ?variance_ge0//=. - by rewrite compre_scale ?integrableZl. - rewrite [X in EFin \o X](_ : _ = r ^+2 \o* X ^+ 2)%R 1?mulrACA//. by rewrite compre_scale ?integrableZl. - by rewrite -mulrAC 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