proposition: Lemma step6 : 1 - 2 * delta <= esrc(P , sc).
proof: Proof. have H : exp2 (- k.+1%:R * (e0 - delta)) <= delta. apply (@Log_le_inv 2) => //. - exact Hdelta. - rewrite /exp2 ExpK //. apply (@leR_pmul2r (1 / (e0 - delta))) => //. + apply divR_gt0; first lra. apply subR_gt0. rewrite /e0 /delta /r. have H1 : (`H P - r) / 2 < `H P - r. rewrite -[X in _ < X]mulR1. apply ltR_pmul2l; last lra. by apply/RltP; rewrite RminusE subr_gt0; apply/RltP; case: Hr. apply Rmin_case_strong => H2 //; exact: (leR_ltR_trans H2 H1). + rewrite -mulRA div1R mulRV; last by rewrite subR_eq0'; exact/eqP/e0_delta. rewrite mulNR mulR1 leR_oppl. by move: Hk => /leR_max[] /leR_max[]. suff : 1 - (esrc(P , sc)) <= delta + delta by move=> *; lra. exact/(leR_trans step5)/leR_add2l. 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