proposition: Lemma sum_rV_ffun (I J : finType) (F : {ffun I -> J} -> R) (G : _ -> _ -> _) (idef : I) (zero : 'I_ _) : O = zero -> \big[+%M/0]_(j : 'rV[J]_#|I|) G (F [ffun x => j ord0 (enum_rank x)]) (j ord0 zero) = \big[+%M/0]_(f : {ffun I -> J}) G (F f) (f (nth idef (enum I) 0)).
proof: Proof. Local Open Scope ring_scope. move=> Hzero. rewrite (reindex_onto (fun y : {ffun _ -> J} => \row_(i < _) y (enum_val i)) (fun p => [ffun x => p ord0 (enum_rank x)])) //. apply eq_big. move=> t /=. apply/eqP/ffunP => i'. by rewrite ffunE mxE enum_rankK. move=> i Hi. rewrite /= in Hi. rewrite (eqP Hi). f_equal. by rewrite mxE (enum_val_nth idef) -Hzero. move=> i _. apply/rowP => a; by rewrite mxE ffunE enum_valK. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix perm) Reals Lra Classical mathcomp(Rstruct classical_sets) ssrZ ssrR Reals_ext realType_ext logb ssr_ext ssralg_ext bigop_ext fdist proba entropy aep typ_seq joint_typ_seq channel channel_code