proposition: Lemma schaE (W : `Ch(A, B)) (c : code) : scha(W, c) = (1 / #|M|%:R * \sum_(m : M) \sum_(tb | dec c tb == Some m) (W ``(| enc c m)) tb)%R.
proof: Proof. set rhs := (\sum_(m | _ ) _)%R. have {rhs}-> : rhs = (\sum_(m in M) (1 - e(W, c) m))%R. apply eq_bigr => i Hi; rewrite -Pr_to_cplt. apply eq_bigl => t /=; by rewrite inE. set rhs := (\sum_(m | _ ) _)%R. have {rhs}-> : rhs = (#|M|%:R - \sum_(m in M) e(W, c) m)%R. by rewrite /rhs {rhs} big_split /= big_const iter_addR mulR1 -big_morph_oppR. by rewrite mulRDr -mulRA mulVR ?mulR1 ?INR_eq0' -?lt0n // mulRN. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) Reals mathcomp(Rstruct) Reals_ext ssrR logb fdist proba channel