proposition: Lemma v_scode' : exists sc : scode_vl _ n, cancel (enc sc) (dec sc) /\ @E_leng_cw _ _ P (enc sc) / INR n < `H P + epsilon.
proof: Proof. move : (fdist_supp_lg_add_1_neq_0 P) => ?. exists (mkScode (f P epsilon') (phi n' P epsilon')). apply: conj=> [ x |]; first by apply: (phi_f _ eps'_pos). apply: (Rmult_lt_reg_r (INR n)); first by apply: lt_0_INR; apply/ltP. rewrite /Rdiv -mulRA -(mulRC (INR n)) mulRV ?INR_eq0' // mulR1. apply: (Rle_lt_trans _ (IZR (L_typ n' P epsilon') + 1 + epsilon' * (IZR (L_not_typ X n') + 1))). - by apply: E_leng_cw_le_Length; [apply: eps'_pos | apply: le_aepbound_n]. - by apply: lb_entro_plus_eps. Qed.
imports: mathcomp(all_ssreflect ssralg matrix) Reals Lra mathcomp(Rstruct) ssrR Reals_ext realType_ext logb ssr_ext ssralg_ext bigop_ext fdist proba entropy aep typ_seq natbin source_code