proposition: Theorem source_coding_converse : forall epsilon, 0 < epsilon < 1 -> forall r : Qplus, 0 < r < `H P -> forall n k (sc : scode_fl A k.+1 n), SrcRate sc = r -> SrcConverseBound P (num r) (den r) n epsilon <= k.+1%:R -> epsilon <= esrc(P , sc).
proof: Proof. move=> epsilon Hespilon r r_HP n k sc r_sc Hk_bound. exact: (@source_coding_converse' _ _ (num r) (den r)). Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) Reals Lra mathcomp(Rstruct) ssrR Reals_ext realType_ext logb fdist proba entropy aep typ_seq source_code