proposition: Lemma step5 : 1 - (esrc(P , sc)) <= delta + exp2 (- k.+1%:R * (e0 - delta)).
proof: Proof. apply (@leR_trans (delta + #| no_failure |%:R * exp2 (- k.+1%:R * (`H P - delta)))). - apply/(leR_trans step4)/leR_add2l/leR_wpmul2r => //. exact/le_INR/leP/subset_leqif_cards/subsetIl. - apply leR_add2l. apply (@leR_trans (exp2 (k.+1%:R * (`H P - e0)) * exp2 (- k.+1%:R * (`H P - delta)))); last first. rewrite -ExpD; apply Exp_le_increasing => //; apply Req_le; by field. apply leR_wpmul2r => //; exact no_failure_sup. 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