proposition: Lemma rprod_rsum_commute d (B : finType) (x : 'rV_n) (W: `Ch('F_2, B)) m0 n0 (m0n0 : n0 \in 'V m0) : let pr n1 t := (dprojs_V H d n1 t \in pfamily d (`F n1 :\ m0) (fun m1 => freeon (`V(m1, n1) :\ n1) d)) && (comb_V H d n1 (dprojs_V H d n1 t) == t) in let g := dprojs_V2 H d m0 n0 in let g' := comb_V2 H d m0 n0 in (\prod_(n1 in 'V m0 :\ n0) (\sum_(t | pr n1 t) W (t ``_ n1) (x ``_ n1) * \prod_(m1 in `F n1 :\ m0) (W ``(x \# `V(m1, n1) :\ n1 | ((dprojs_V H d n1 t) m1) \# `V(m1, n1) :\ n1) * \prod_(m2 in `F(m1, n1)) INR (\delta ('V m2) ((dprojs_V H d n1 t) m1)))) = \sum_(t | (g t \in pfamily d ('V m0 :\ n0) pr) && (g' (g t) == t)) \prod_(n1 in 'V m0 :\ n0) (W ((g t n1) ``_ n1) (x ``_ n1) * \prod_(m1 in `F n1 :\ m0) (W ``(x \# `V(m1, n1) :\ n1 | ((dprojs_V H d n1 (g t n1)) m1) \# `V(m1, n1) :\ n1) * \prod_(m2 in `F(m1, n1)) INR (\delta ('V m2) ((dprojs_V H d n1 (g t n1)) m1)))))%R.
proof: Proof. move=> pr g g'. rewrite (big_distr_big_dep d) /=. rewrite (reindex_onto (dprojs_V2 H d m0 n0) (comb_V2 H d m0 n0)) //. move=> /= t' Ht'. rewrite /dprojs_V2 /comb_V2. apply/ffunP => /= n1. apply/rowP => n2. case/boolP : (n2 \in ssgraph H m0 n0 n1). rewrite inE; case/andP => Hn1 /existsP [] m1 Hm1. rewrite dprojs_in => /=; last first. rewrite /ssgraph Hn1 /= inE. apply/existsP; exists m1; by rewrite Hm1. move H0 : [pick a | n2 \in ssgraph H m0 n0 a] => [n1'|]; last first. case: pickP H0 => //. move/(_ n1); rewrite inE Hn1 /= => /negbT; rewrite negb_exists => /forallP/(_ m1). by rewrite Hm1. have ? : n1' = n1. case: pickP H0 => // x0. rewrite inE => /andP[Hn1' H0]. move: H0 => /existsP[m1' /andP[Hm1' Hn2']]. case/andP : Hm1 => Hm1 Hn2 [<-]. by rewrite (Vgraph_id Hacyclic m0n0 Hn1 Hn1' Hm1 Hm1' Hn2 Hn2'). subst n1'. by rewrite (@comb_in _ _ d _ t' (ssgraph H m0 n0) _ n1). rewrite inE negb_and. case/orP => [Hn1|]. rewrite dprojs_out /=; last by rewrite inE negb_and Hn1. case/pfamilyP : Ht' => Ht' _. move/supportP : Ht'. by move/(_ n1 Hn1) => ->. move=> tmp. case/boolP : (n1 \in 'V m0 :\ n0) => Hn1; last first. rewrite dprojs_out //; last by rewrite inE /ssgraph (negbTE Hn1). case/pfamilyP : (Ht'). by move/supportP => /(_ _ Hn1) ->. case/pfamilyP : (Ht') => _ /(_ _ Hn1). rewrite {1}/in_mem /=. case/andP => H1 /eqP <-. rewrite dprojs_out //; last by rewrite inE /ssgraph Hn1. rewrite (comb_V_support _ tmp) //; by case/pfamilyP : H1. 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