proposition: Lemma ELC_TupleFDist : @E_leng_cw _ _ (P `^ n) fm = m%:R * @E_leng_cw _ _ P f.
proof: Proof. rewrite /E_leng_cw /= /fm. pose X := INR \o size \o f. elim: m => [|m']. rewrite mul0R /Ex big1 // => i _. rewrite fdist_rV0 ?mulR1. rewrite /comp_RV. rewrite [tuple_of_row]lock /= -lock. rewrite (_ : tuple_of_row i = [tuple]) //. apply: eq_from_tnth. by case; case. elim: m' => [_ |m'' _ IH]. rewrite mul1R. rewrite -[in RHS]E_cast_RV_fdist_rV1. apply: eq_bigr => i _. rewrite fdist_rV1; congr (_ * _). rewrite /comp_RV. rewrite [tuple_of_row]lock /= -lock. rewrite (_ : tuple_of_row i = [tuple of [:: i ``_ ord0]]); last first. by apply eq_from_tnth => a; rewrite {a}(ord1 a) tnth_mktuple. by rewrite /extension /= cats0. pose fm1 (x : 'rV['rV[A]_n]_(m''.+1)) := extension f (tuple_of_row x). pose Xm1 := INR \o size \o fm1. pose fm2 (x : 'rV['rV[A]_n]_(m''.+2)) := extension f (tuple_of_row x). pose Xm2 := INR \o size \o fm2. have X_Xm1_Xm2 : Xm2 \= X @+ Xm1. rewrite /Xm2 => x /=. rewrite -plus_INR plusE -size_cat. rewrite /fm2 /extension /fm1 /extension. rewrite [tuple_of_row]lock /= -lock. congr ((size _)%:R). rewrite {1}(_ : x = row_mx (\row_(i < 1) (x ``_ ord0)) (rbehead x)); last first. apply/matrixP => a b; by rewrite {}(ord1 a) row_mx_rbehead. rewrite (@tuple_of_row_row_mx _ _ _ (\row_(i < 1) (x ``_ ord0)) (rbehead x)). rewrite map_cat flatten_cat. congr (_ ++ _). rewrite (_ : tuple_of_row _ = [tuple of [:: x ``_ ord0]]); last first. by apply eq_from_tnth => i; rewrite {i}(ord1 i) /= tnth_mktuple mxE. by rewrite /= cats0. rewrite (E_sum_2 X_Xm1_Xm2) S_INR mulRDl -IH addRC; congr (_ + _)%R. by rewrite /Xm1 -/fm1 /Ex tail_of_fdist_rV_fdist_rV. by rewrite -/X mul1R /Ex head_of_fdist_rV_fdist_rV. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) Reals mathcomp(Rstruct) ssrR Reals_ext realType_ext logb ssr_ext ssralg_ext bigop_ext fdist proba entropy divergence log_sum source_code