proposition: Lemma rmul_rsum_commute0 d n0 (B : finType) (t : 'rV[B]_n) (W : forall m, 'rV_m -> 'rV_m -> R) (F : 'I_m -> 'rV_n -> R) (HF : forall m1 m0 (t' : 'rV_n), m1 \in 'F(m0, n0) -> t' ``_ n0 = d ``_ n0 -> F m1 ((dprojs_V H d n0 t') m0) = F m1 t') : \prod_(m0 in 'F n0) (\sum_(t' = d [~'V(m0, n0) :\ n0]) W _ (t \# 'V(m0, n0) :\ n0) (t' \# 'V(m0, n0) :\ n0) * \prod_(m1 in 'F(m0, n0)) F m1 t') = \sum_(t' = d [~ setT :\ n0]) (\prod_(m0 in 'F n0) (W _ (t \# 'V(m0, n0) :\ n0) (t' \# 'V(m0, n0) :\ n0) * \prod_(m1 in 'F(m0, n0)) F m1 t')).
proof: Proof. rewrite (big_distr_big_dep d [pred x in 'F n0] (fun i => freeon ('V(i, n0) :\ n0) d)) [LHS]/=. rewrite (reindex_onto (dprojs_V H d n0) (comb_V H d n0)); last first. rewrite /= => f Hf; by apply (@dprojs_comb_V d n0 (fun n => 'F n)). rewrite [LHS]/=. apply/esym/eq_big. - move=> /= t'. case Hlhs : (freeon _ _ t'). apply/esym. rewrite comb_dprojs_V => //; last first. by rewrite (freeon_notin Hlhs) // !inE eqxx. by rewrite eqxx andbT pfamily_dprojs_V. apply/esym/negbTE. move/negbT : Hlhs; apply contra. case/andP => _ /eqP <-. by rewrite freeon_comb_dprojs_V. - move=> /= t' Ht'. apply eq_bigr => m0 Hm0. congr (_ * _)%R. + by rewrite /dprojs_V sub_vec_dprojs. + apply eq_bigr => m1 Hm1. by rewrite HF // -(freeon_notin Ht') //= !inE eqxx. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg zmodp matrix) Reals mathcomp(Rstruct) ssr_ext ssralg_ext ssrR Reals_ext f2 summary subgraph_partition tanner tanner_partition fdist channel checksum