fact: Definition success_factor (tc : typed_code B M P) (V : P_ n (A , B)) := exp2 (- n%:R * `H(V | P)) / #|M|%:R * \sum_ (m : M) #| (V.-shell (tuple_of_row (enc tc m ))) :&: (@tuple_of_row B n @: ((dec tc) @^-1: [set Some m])) |%:R.
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