proposition: Lemma typed_success (tc : typed_code B M P) : scha(W, tc) = \sum_ (V | V \in \nu^{B}(P)) exp_cdiv P V W * success_factor tc V.
proof: Proof. rewrite schaE // div1R. symmetry. transitivity (/ #|M|%:R * \sum_(m : M) \sum_(V | V \in \nu^{B}(P)) exp_cdiv P V W * #| V.-shell (tuple_of_row (enc tc m)) :&: (@tuple_of_row B n @: (dec tc @^-1: [set Some m])) |%:R * exp2 (- n%:R * `H(V | P))). rewrite exchange_big /= big_distrr /=. apply eq_bigr => V _. rewrite /success_factor !mulRA -(mulRC (/ #|M|%:R)) -!mulRA; f_equal. symmetry; rewrite -big_distrl /= -big_distrr /= -mulRA; f_equal. by rewrite mulRC. f_equal. apply eq_bigr=> m _. rewrite (reindex_onto (@row_of_tuple B n) (@tuple_of_row B n)); last first. move=> i Hi; by rewrite tuple_of_rowK. rewrite (sum_tuples_ctypes (typed_prop tc m)) //. apply eq_bigr=> V HV. rewrite -mulRA mulRC -mulRA -iter_addR -big_const. apply eq_big => tb. - rewrite inE row_of_tupleK eqxx andbT. f_equal. apply/imsetP/idP. case=> v H ->; rewrite tuple_of_rowK. by rewrite 2!inE in H. move=> Hm. exists (row_of_tuple tb); last by rewrite row_of_tupleK. by rewrite !inE. - rewrite in_set. move=> /andP [Htb _]. rewrite mulRC -(@dmc_exp_cdiv_cond_entropy _ _ _ _ _ _ _ (row_of_tuple tb) (typed_prop tc m) HV) //. by rewrite row_of_tupleK. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) Reals mathcomp(Rstruct) ssrR Reals_ext ssr_ext ssralg_ext logb fdist entropy ln_facts num_occ types jtypes divergence conditional_divergence entropy channel_code channel