proposition: Lemma rprod_sub_vec (D : {set 'I_n}) (t : 'rV_n) : \prod_(i < #|D|) W ((t \# D) ``_ i) ((tb \# D) ``_ i) = \prod_(i in D) W (t ``_ i) (tb ``_ i).
proof: Proof. have [->|/set0Pn[i iD]] := eqVneq D set0. by rewrite big_set0 big_hasC //; apply/hasPn => /=; rewrite cards0; case. pose f : 'I_n -> 'I_#|D| := fun i => match Bool.bool_dec (i \in D) true with | left H => enum_rank_in H i | _ => enum_rank_in iD i end. rewrite (reindex_onto (fun i : 'I_#|D| => enum_val i) f) /=. apply: eq_big => j; last by rewrite /sub_vec 2!mxE. rewrite /f /=; case: Bool.bool_dec => [a|]. by rewrite enum_valK_in a eqxx. by rewrite enum_valP. move=> j jD. by rewrite /f /=; case: Bool.bool_dec => [a| //]; rewrite enum_rankK_in. Qed.
imports: mathcomp(all_ssreflect all_algebra) Reals mathcomp(Rstruct) ssrR Reals_ext logb ssr_ext ssralg_ext bigop_ext fdist proba entropy jfdist_cond