proposition: Lemma E_id_rem : X \= X1 @+ X2 -> P |= X1' _|_ X2' -> `E (X `^2) = `E (X1 `^2) + 2 * `E X1 * `E X2 + `E (X2 `^2).
proof: Proof. move=> Hsum Hinde. rewrite -![in RHS]Ex_altE. transitivity (\sum_(i in 'rV_n.+2) ((X1 (i ``_ ord0) + X2 (rbehead i)) ^ 2%N * P i)). apply eq_bigr => i _; rewrite /sq_RV /=. by rewrite /comp_RV Hsum. transitivity (\sum_(i in 'rV_n.+2) ((X1 (i ``_ ord0)) ^ 2 + 2 * X1 (i ``_ ord0) * X2 (rbehead i) + (X2 (rbehead i)) ^ 2) * P i). apply eq_bigr => ? _; by rewrite sqrRD. transitivity (\sum_(i in 'rV_n.+2) ((X1 (i ``_ ord0)) ^ 2 * P i + 2 * X1 (i ``_ ord0) * X2 (rbehead i) * P i + (X2 (rbehead i)) ^ 2 * P i)). apply eq_bigr => ? ?; by field. rewrite !big_split /=; congr (_ + _ + _). - rewrite Ex_altE -(big_rV_cons_behead _ xpredT xpredT) /=. apply eq_bigr => i _. transitivity (X1 i ^ 2 * \sum_(j in 'rV_n.+1) (fdist_prod_of_rV P) (i, j)). + rewrite big_distrr /=; apply eq_bigr => i0 _. by rewrite row_mx_row_ord0 fdist_prod_of_rVE. + by rewrite fdist_fstE. - rewrite -mulRA. rewrite !Ex_altE. rewrite -E_id_rem_helper // big_distrr /=. apply eq_bigr => i _; field. - rewrite Ex_altE -(big_rV_cons_behead _ xpredT xpredT) exchange_big /=. apply eq_bigr => t _. transitivity (X2 t ^ 2 * \sum_(i in A) (fdist_prod_of_rV P) (i, t)). + rewrite big_distrr /=; apply eq_bigr => i _. by rewrite rbehead_row_mx fdist_prod_of_rVE. + by congr (_ * _); rewrite fdist_sndE. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) mathcomp(Rstruct reals) Reals Lra ssrR Reals_ext realType_ext logb ssr_ext ssralg_ext bigop_ext fdist