proposition: Lemma JTS_1 : (JTS_1_bound <= n)%nat -> 1 - epsilon <= Pr ((P `X W) `^ n) (`JTS P W n epsilon).
proof: Proof. have : (JTS_1_bound <= n)%nat -> Pr ( (P `^ n `X (W ``^ n)) ) [set x | x.1 \notin `TS P n epsilon] + Pr ( (P `^ n `X (W ``^ n)) ) [set x | x.2 \notin `TS (`O(P , W)) n epsilon] + Pr ( (P `^ n `X (W ``^ n))) [set x | prod_rV x \notin `TS ( (P `X W) ) n epsilon] <= epsilon. have H1 : forall n, Pr ((P `X W) `^ n) [set x | (rV_prod x).1 \notin `TS P n epsilon ] <= Pr (P `^ n) [set x | x \notin `TS P n (epsilon / 3)]. move=> m. have : 1 <= 3 by lra. move/(set_typ_seq_incl P m (ltRW He)) => Hincl. rewrite (Pr_DMC_fst P W (fun x => x \notin `TS P m epsilon)). apply/Pr_incl/subsetP => i /=; rewrite !inE. apply contra. by move/subsetP : Hincl => /(_ i); rewrite !inE. have {H1}HnP : forall n, ('| up (aep_bound P (epsilon / 3)) | <= n)%nat -> Pr ((P `X W) `^ n) [set x | (rV_prod x).1 \notin `TS P n epsilon ] <= epsilon /3. move=> m Hm. apply: leR_trans; first exact: (H1 m). have m_prednK : m.-1.+1 = m. rewrite prednK // (leq_trans _ Hm) // (_ : O = '| 0 |) //. by apply/ltP/Zabs_nat_lt; split; [by [] | apply/up_pos/aep_bound_ge0; lra]. have : 1 - (epsilon / 3) <= Pr (P `^ m) (`TS P m (epsilon/3)). rewrite -m_prednK. apply Pr_TS_1. - by apply divR_gt0 => //; lra. - rewrite m_prednK. move/leP/le_INR : Hm; apply leR_trans. rewrite INR_Zabs_nat; last first. apply/ltZW/up_pos/aep_bound_ge0 => //. apply divR_gt0 => //; lra. exact/ltRW/(proj1 (archimed _ )). rewrite leR_subl_addr addRC -leR_subl_addr; apply: leR_trans. rewrite Pr_to_cplt setCK. by apply/RleP; rewrite Order.POrderTheory.lexx. have H1 m : Pr ((P `X W) `^ m) [set x | (rV_prod x).2 \notin `TS ( `O(P , W) ) m epsilon ] <= Pr ( (`O( P , W) ) `^ m) (~: `TS ( `O( P , W) ) m (epsilon / 3)). have : 1 <= 3 by lra. move/(set_typ_seq_incl (`O(P , W)) m (ltRW He)) => Hincl. rewrite Pr_DMC_out. apply/Pr_incl/subsetP => i /=; rewrite !inE. apply contra. move/subsetP : Hincl => /(_ i). by rewrite !inE. have {H1}HnPW m : ('| up (aep_bound (`O(P , W)) (epsilon / 3)) | <= m)%nat -> Pr ((P `X W) `^ m) [set x | (rV_prod x).2 \notin `TS (`O(P , W)) m epsilon] <= epsilon /3. move=> Hm. apply: leR_trans; first exact: (H1 m). have m_prednK : m.-1.+1 = m. rewrite prednK // (leq_trans _ Hm) // (_ : O = '| 0 |) //. apply/ltP/Zabs_nat_lt ; split; [by []|apply/up_pos/aep_bound_ge0; lra]. have : 1 - epsilon / 3 <= Pr ((`O(P , W)) `^ m) (`TS (`O(P , W)) m (epsilon / 3)). rewrite -m_prednK. apply Pr_TS_1. - apply divR_gt0 => //; lra. - move/leP/le_INR : Hm. rewrite m_prednK. apply leR_trans. rewrite INR_Zabs_nat; last first. apply/ltZW/up_pos/aep_bound_ge0; lra. exact/ltRW/(proj1 (archimed _ )). rewrite leR_subl_addr addRC -leR_subl_addr; apply: leR_trans. rewrite Pr_to_cplt setCK. by apply/RleP; rewrite Order.POrderTheory.lexx. have H1 m : Pr ((P `X W) `^ m) (~: `TS ((P `X W)) m epsilon) <= Pr (((P `X W) ) `^ m) (~: `TS ((P `X W)) m (epsilon / 3)). have : 1 <= 3 by lra. move/(set_typ_seq_incl ((P `X W)) m (ltRW He)) => Hincl. apply/Pr_incl/subsetP => /= v; rewrite !inE. apply contra. by move/subsetP : Hincl => /(_ v); by rewrite !inE. have {H1}HnP_W m : ('| up (aep_bound ((P `X W)) (epsilon / 3)) | <= m)%nat -> Pr ((P `X W) `^ m) (~: `TS ((P `X W)) m epsilon) <= epsilon /3. move=> Hm. apply: leR_trans; first exact: (H1 m). have m_prednK : m.-1.+1 = m. rewrite prednK // (leq_trans _ Hm) // (_ : O = '| 0 |) //. apply/ltP/Zabs_nat_lt; split; [by []|apply/up_pos/aep_bound_ge0; lra]. have : 1 - epsilon / 3 <= Pr (((P `X W)) `^ m) (`TS ((P `X W)) m (epsilon / 3)). rewrite -m_prednK; apply Pr_TS_1. - apply divR_gt0 => //; lra. - rewrite m_prednK. move/leP/le_INR : Hm; apply leR_trans. rewrite INR_Zabs_nat; last first. apply/ltZW/up_pos/aep_bound_ge0; lra. exact/Rlt_le/(proj1 (archimed _ )). rewrite leR_subl_addr addRC -leR_subl_addr; apply: leR_trans. rewrite Pr_to_cplt setCK. by apply/RleP; rewrite Order.POrderTheory.lexx. move=> Hn. rewrite [in X in _ <= X](_ : epsilon = epsilon / 3 + epsilon / 3 + epsilon / 3)%R; last by field. move: Hn; rewrite 2!geq_max => /andP[Hn1 /andP[Hn2 Hn3]]. rewrite !Pr_DMC_rV_prod. apply leR_add; first by apply leR_add; [exact: HnP | exact: HnPW]. apply: leR_trans; last exact/HnP_W/Hn3. by apply/Req_le; congr Pr; apply/setP => /= tab; by rewrite !inE rV_prodK. move=> Hn_Pr Hn. suff H : Pr ((P `X W) `^ n ) (~: `JTS P W n epsilon) <= epsilon. rewrite -(Pr_cplt ((P `X W) `^ n) (`JTS P W n epsilon)). by rewrite leR_subl_addr leR_add2l. apply (@leR_trans (Pr ((P `X W) `^ n) ([set x | ((rV_prod x).1 \notin `TS P n epsilon)] :|: ([set x | ((rV_prod x).2 \notin `TS (`O( P , W)) n epsilon)] :|: (~: `TS ((P `X W)) n epsilon))))). by apply Req_le; congr Pr; apply/setP => xy; rewrite !inE 2!negb_and orbA. apply: leR_trans; last exact: Hn_Pr. apply (@leR_trans ( Pr ((P `X W) `^ n) [set x | (rV_prod x).1 \notin `TS P n epsilon] + Pr ((P `X W) `^ n) ([set x | ((rV_prod x).2 \notin `TS (`O( P , W)) n epsilon)] :|: (~: `TS ((P `X W)) n epsilon)))). exact: Pr_union. rewrite -addRA !Pr_DMC_rV_prod; apply/leR_add2l; apply: leR_trans (Pr_union _ _ _). by apply/Req_le; congr Pr; apply/setP => t; rewrite !inE rV_prodK. Qed.
imports: mathcomp(all_ssreflect ssralg matrix) Reals Lra mathcomp(Rstruct) ssrZ ssrR Reals_ext ssr_ext logb ssralg_ext bigop_ext fdist proba entropy aep typ_seq channel