proposition: Lemma step4 : 1 - (esrc(P , sc)) <= delta + #| no_failure :&: `TS P k.+1 delta|%:R * exp2 (- k.+1%:R * (`H P - delta)).
proof: Proof. apply/(leR_trans step3)/leR_add. - move: Hk => /leR_max[] /leR_max[]. move/(Pr_TS_1 Hdelta) => Hdelta _ _. rewrite -[in X in _ <= X](oppRK delta) leR_oppr -(@leR_add2l 1) 2!addR_opp. move/leR_trans : Hdelta; apply. rewrite Pr_to_cplt. by apply/RleP; rewrite lexx. - apply (@leR_trans (\sum_(x in 'rV[A]_k.+1 | x \in no_failure :&: `TS P k.+1 delta) exp2 (- k.+1%:R * (`H P - delta)))). apply leR_sumR => /= i. rewrite in_setI => /andP[i_B i_TS]. move: (typ_seq_definition_equiv2 i_TS) => [H1 _]. apply (@Log_le_inv 2) => //. + move: i_TS. rewrite /`TS inE /typ_seq => /andP[/RleP i_TS _]. exact: (ltR_leR_trans (exp2_gt0 _) i_TS). + rewrite /exp2 ExpK //. rewrite mulRC mulRN -mulNR -leR_pdivr_mulr; last exact/ltR0n. rewrite leR_oppr /Rdiv mulRC; by rewrite div1R mulNR in H1. rewrite big_const iter_addR. by apply/RleP; rewrite lexx. 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