proposition: Theorem source_coding_direct epsilon : 0 < epsilon < 1 -> forall r : Qplus, `H P < r -> exists k n (sc : scode_fl A k n), SrcRate sc = r /\ esrc(P , sc) <= epsilon.
proof: Proof. move=> Heps re HP_r; destruct re as [num den]. by exists (k P num den epsilon), (n P num den epsilon); exact: source_coding'. Qed.
imports: mathcomp(all_ssreflect ssralg matrix) Reals Lra mathcomp(Rstruct) ssrZ ssrR Reals_ext ssr_ext ssralg_ext logb natbin fdist proba entropy aep typ_seq source_code