proposition: Lemma Pr_TS_1 : aep_bound P epsilon <= n.+1%:R -> 1 - epsilon <= Pr (P `^ n.+1) (`TS P n.+1 epsilon).
proof: Proof. move=> k0_k. have -> : Pr P `^ n.+1 (`TS P n.+1 epsilon) = Pr P `^ n.+1 [set i | (i \in `TS P n.+1 epsilon) && (0 < P `^ n.+1 i)%mcR]. congr Pr; apply/setP => /= t; rewrite !inE. apply/idP/andP => [H|]; [split => // | by case]. case/andP : H => /RleP H _; exact/RltP/(ltR_leR_trans (exp2_gt0 _) H). set p := [set _ | _]. rewrite Pr_to_cplt leR_add2l leR_oppl oppRK. have -> : Pr P `^ n.+1 (~: p) = Pr P `^ n.+1 [set x | P `^ n.+1 x == 0] + Pr P `^ n.+1 [set x | (0 < P `^ n.+1 x)%mcR && (`| - (1 / n.+1%:R) * log (P `^ n.+1 x) - `H P | > epsilon)%mcR]. have -> : ~: p = [set x | P `^ n.+1 x == 0 ] :|: [set x | (0 < P `^ n.+1 x)%mcR && (`| - (1 / n.+1%:R) * log (P `^ n.+1 x) - `H P | > epsilon)%mcR]. apply/setP => /= i; rewrite !inE negb_and orbC. apply/idP/idP => [/orP[/RltP|]|]. - move/RltP => H. have {}H : P `^ n.+1 i = 0. apply/eqP. apply/negPn. apply: contra H. by have [+ _] := fdist_gt0 (P `^ n.+1) i. by rewrite H eqxx. - rewrite /typ_seq negb_and => /orP[|] LHS. + have [//|H1] := eqVneq (P `^ n.+1 i) 0. have {}H1 : 0 < P `^ n.+1 i by apply/RltP; rewrite lt0r H1/=. apply/andP; split; first exact/RltP. move/RleP: LHS => /ltRNge/(@Log_increasing 2 _ _ Rlt_1_2 H1). rewrite /exp2 ExpK // mulRC mulRN -mulNR -ltR_pdivr_mulr; last exact/ltR0n. rewrite /Rdiv mulRC ltR_oppr => /RltP; rewrite -ltrBrDl => LHS. rewrite div1r// mulNr -RinvE//; last by rewrite gt_eqF// ltr0n. rewrite ger0_norm// -INRE//. by move/RltP : LHS; move/(ltR_trans He)/ltRW/RleP. + move: LHS; rewrite leNgt negbK => LHS. apply/orP; right; apply/andP; split. exact/(lt_trans _ LHS)/RltP/exp2_gt0. move/RltP in LHS. move/(@Log_increasing 2 _ _ Rlt_1_2 (exp2_gt0 _)) : LHS. rewrite /exp2 ExpK // mulRC mulRN -mulNR -ltR_pdivl_mulr; last exact/ltR0n. rewrite oppRD oppRK => LHS. have H2 : forall a b c, - a + b < c -> - c - a < - b by move=> *; lra. move/H2 in LHS. rewrite div1r mulrC mulrN ler0_norm//. * rewrite ltrNr//; apply/RltP; rewrite -RminusE -RoppE. by rewrite -RdivE ?gt_eqF// ?ltr0n// -INRE. * apply/RleP; rewrite -RminusE -RoppE. rewrite -RdivE ?gt_eqF// ?ltr0n// -INRE//. apply: (leR_trans (ltRW LHS)). by apply/RleP; rewrite lerNl oppr0// ltW//; apply/RltP. - rewrite -negb_and; apply: contraTN. rewrite negb_or /typ_seq => /andP[H1 /andP[/RleP H2 /RleP H3]]. apply/andP; split; first exact/gtR_eqF/RltP. rewrite negb_and H1 /= -leNgt. move/(@Log_increasing_le 2 _ _ Rlt_1_2 (exp2_gt0 _)) : H2. rewrite /exp2 ExpK // mulRC mulRN -mulNR -leR_pdivl_mulr ?oppRD; last exact/ltR0n. move => H2. have /(_ _ _ _ H2) {}H2 : forall a b c, - a + - b <= c -> - c - a <= b. by move=> *; lra. move/RltP in H1. move/(@Log_increasing_le 2 _ _ Rlt_1_2 H1) : H3. rewrite /exp2 ExpK //. rewrite mulRC mulRN -mulNR -leR_pdivr_mulr; last exact/ltR0n. rewrite oppRD oppRK div1r mulrC mulrN => H3. have /(_ _ _ _ H3) {}H3 : forall a b c, a <= - c + b -> - b <= - a - c. by move=> *; lra. by rewrite ler_norml; apply/andP; split; apply/RleP; rewrite -RminusE -RoppE; rewrite -RdivE ?gt_eqF// ?ltr0n// -INRE//. rewrite Pr_union_disj // disjoints_subset; apply/subsetP => /= i. by rewrite !inE /= => /eqP Hi; rewrite negb_and Hi ltxx. rewrite {1}/Pr (eq_bigr (fun=> 0)); last by move=> /= v; rewrite inE => /eqP. rewrite big_const iter_addR mulR0 add0R. apply/(leR_trans _ (aep He k0_k))/Pr_incl/subsetP => /= t. rewrite !inE /= => /andP[-> H3]. rewrite /log_RV /= /scalel_RV /= mulRN -mulNR. apply/ltW. by rewrite RmultE RoppE// RdivE ?gt_eqF ?INRE ?ltr0n. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) Reals Lra mathcomp(Rstruct) ssrR Reals_ext realType_ext logb fdist proba entropy aep