proposition: Lemma summary_powersetE (s : {set 'I_n}) (d : 'rV['F_2]_n) (e : 'rV['F_2]_n -> R) : \sum_(t = d [~s]) e t = summary_powerset s d e.
proof: Proof. rewrite /summary_powerset. transitivity (\sum_(f in {ffun 'I_n -> 'F_2} | freeon s (\row_i f i) d) e (\row_(k0 < n) if k0 \in s then (fgraph f) !_ (cast_ord (esym (@card_ord n)) k0) else d ``_ k0))%R. rewrite (reindex_onto (fun p => [ffun x => p !_ (cast_ord (esym (@card_ord n)) x)]) (fun y => fgraph y)) /=; last first. move=> /= f Hf. apply/ffunP => /= k0. by rewrite ffunE -enum_rank_ord tnth_fgraph enum_rankK. rewrite (reindex_onto (fun p => row_of_tuple (tcast (@card_ord n) p)) (fun y => tcast (esym (@card_ord n)) (tuple_of_row y))) /=; last first. move=> k0 Hk0. apply/rowP => b. by rewrite !mxE 2!tcastE tnth_mktuple esymK -enum_rank_ord -enum_val_ord enum_rankK. apply eq_big. move=> t. congr (_ && _). rewrite freeon_sym; congr (freeon s _ d). apply/rowP => i; by rewrite !mxE ffunE tcastE. congr (_ == t); apply eq_from_tnth => i /=. rewrite !tcastE tnth_mktuple mxE tcastE tnth_fgraph ffunE. by rewrite esymK -enum_val_ord. move=> t Ht. congr e. apply/rowP => b; rewrite !mxE. case/boolP : (b \in s) => bs. by rewrite tnth_fgraph ffunE tcastE enum_val_ord cast_ordK. rewrite tcastE. case/andP : Ht => Ht1 Ht2. move/forallP : Ht1. move/(_ b). rewrite bs implyTb. move/eqP => ->. by rewrite /row_of_tuple mxE tcastE. transitivity (\sum_(f in {ffun 'I_n -> bool} | freeon s d (\row_i F2_of_bool (f i))) e (\row_k0 (if k0 \in s then F2_of_bool ((fgraph f) !_ (cast_ord (esym (card_ord n)) k0)) else d ``_ k0)))%R. rewrite (reindex_onto (fun f : {ffun 'I_n -> bool} => [ffun x => F2_of_bool (f x)]) (fun f : {ffun 'I_n -> 'F_2} => [ffun x => bool_of_F2 (f x)])); last first. move=> /= f Hf. apply/ffunP => /= k0. by rewrite !ffunE bool_of_F2K. apply eq_big. move=> /= f. rewrite freeon_sym -[RHS]andbT; congr (freeon s d _ && _). apply/rowP => i; by rewrite !mxE ffunE. by apply/eqP/ffunP => i; rewrite !ffunE F2_of_boolK. move=> /= f. case/andP => H1 H2. congr e. apply/rowP => b; rewrite !mxE. case : (b \in s) => //. by rewrite 2!tnth_fgraph ffunE. transitivity (\sum_(f in {set 'I_n} | freeon s d (\row_i F2_of_bool (i \in f))) e (\row_k0 (if k0 \in s then F2_of_bool (k0 \in f) else d ``_ k0)))%R. rewrite (reindex_onto (fun f : {ffun 'I_n -> bool} => [set x | f x ]) (@finfun_of_set [finType of 'I_n])). apply eq_big => /= f. rewrite -[LHS]andbT; congr (freeon s d _ && _). apply/rowP => i; by rewrite !mxE inE. apply/esym/eqP/ffunP => /= i; by rewrite SetDef.finsetE ffunE. move=> Hf. congr e. apply/rowP => b; rewrite !mxE. case: (b \in s) => //. by rewrite inE tnth_fgraph -enum_rank_ord enum_rankK. move=> /= f Hf. apply/setP => /= k0. rewrite inE. by rewrite SetDef.pred_of_setE. transitivity (\sum_(f in {set 'I_n} | f \subset s) e (\row_(k0 < n) if k0 \in s then F2_of_bool (k0 \in f) else d ``_ k0))%R; last first. apply eq_bigl => /= s0. by rewrite powersetE. rewrite (reindex_onto (fun f => f :|: [set j | (j \notin s) && bool_of_F2 (d ``_ j)]) (fun f => f :&: s)); last first. move=> /= f fs. apply/setP => /= k0. rewrite !inE. case K : (k0 \in f) => /=; case L : (k0 \in s) => //=; by move/forallP : fs => /(_ k0); rewrite L implyTb mxE K => /eqP ->. apply eq_big => /= s0. apply/andP/subsetP. case=> /forallP H1 H2 /= k0 Hk0. rewrite -(eqP H2) !inE in Hk0. case/andP : Hk0. by case/orP. move=> s0s; split. apply/forallP => /= k0; apply/implyP => Hk0. rewrite mxE !inE Hk0 /=. case K : (k0 \in s0) => /=; last by rewrite bool_of_F2K. move: (s0s k0). by rewrite K (negbTE Hk0) => /(_ erefl). apply/eqP/setP => /= k0; rewrite !inE. case K : (k0 \in s0) => /=; first by apply s0s. by case: (k0 \in s) => //; rewrite andbF. move=> K. congr e. apply/rowP => b; rewrite !mxE. case: ifP => // bs. rewrite !inE. by case : (b \in s0) => //=; rewrite bs. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg zmodp matrix) Reals mathcomp(Rstruct) ssr_ext ssralg_ext ssrR f2