proposition: Theorem source_coding_converse' : epsilon <= esrc(P , sc).
proof: Proof. apply: (leR_trans _ step6). rewrite -[X in _ <= X]oppRK leR_oppr oppRB leR_subl_addr addRC. apply (@leR_pmul2l (/ 2)); first lra. rewrite mulRA mulVR ?mul1R /delta; last exact/eqP. have H1 : lambda / 2 <= / 2 * (1 - epsilon). apply (@leR_trans lambda). by rewrite leR_pdivr_mulr //; apply leR_pmulr; [lra | exact/ltRW/lambda0]. by rewrite /lambda mulRC; exact: geR_minl. apply Rmin_case_strong => ? //; exact: (@leR_trans (lambda / 2)). 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