proposition: Lemma non_typical_sequences : Pr ((P `^ n) `x ((`O(P , W)) `^ n)) [set x | prod_rV x \in `JTS P W n epsilon] <= exp2 (- n%:R * (`I(P, W) - 3 * epsilon)).
proof: Proof. rewrite /Pr /=. apply (@leR_trans (\sum_(i | i \in `JTS P W n epsilon) (exp2 (- INR n * (`H P - epsilon)) * exp2 (- n%:R * (`H( P `o W ) - epsilon))))) => /=. rewrite (reindex_onto (fun y => prod_rV y) (fun x => rV_prod x)) /=; last first. by move=> ? ?; rewrite rV_prodK. apply: leR_sumRl => i; rewrite inE => iJTS. - rewrite fdist_prodE; apply leR_pmul => //. exact: proj2 (typical_sequence1_JTS iJTS). exact: proj2 (typical_sequence1_JTS' iJTS). - exact/mulR_ge0. - by rewrite prod_rVK eqxx andbC. rewrite (_ : \sum_(_ | _) _ = INR #| `JTS P W n epsilon| * exp2 (- n%:R * (`H P - epsilon)) * exp2 (- INR n * (`H( P `o W) - epsilon))); last first. by rewrite big_const iter_addR mulRA. apply (@leR_trans (exp2 (INR n * (`H( P , W ) + epsilon)) * exp2 (- n%:R * (`H P - epsilon)) * exp2 (- INR n * (`H( P `o W ) - epsilon)))). do 2 apply leR_wpmul2r => //. exact/JTS_sup. apply Req_le; rewrite -2!ExpD; congr (exp2 _). rewrite /mutual_info_chan !mulRDr 2!Rmult_opp_opp. by rewrite (_ : 3 * epsilon = epsilon + epsilon + epsilon); field. 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