joint_typ_seq

affeldt-aist · Jan 23, 2025 · 7c8631e · 7c8631e
1 parent 1d3dc1d
commit 7c8631e
Showing 1 changed file with 90 additions and 111 deletions.
diff --git a/information_theory/joint_typ_seq.v b/information_theory/joint_typ_seq.v
@@ -1,9 +1,8 @@
 (* infotheo: information theory and error-correcting codes in Coq             *)
 (* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later            *)
-From mathcomp Require Import all_ssreflect ssrnum ssralg matrix.
-Require Import Reals Lra.
-From mathcomp Require Import Rstruct.
-Require Import ssrZ ssrR Reals_ext ssr_ext logb ssralg_ext bigop_ext.
+From mathcomp Require Import all_ssreflect ssrnum ssrint ssralg matrix.
+From mathcomp Require Import Rstruct reals lra ring archimedean mathcomp_extra.
+Require Import ssr_ext realType_logb ssralg_ext bigop_ext realType_ext.
 Require Import fdist proba entropy aep typ_seq channel.
 
 (******************************************************************************)
@@ -43,12 +42,15 @@ Local Open Scope typ_seq_scope.
 Local Open Scope fdist_scope.
 Local Open Scope channel_scope.
 Local Open Scope entropy_scope.
-Local Open Scope R_scope.
+Local Open Scope ring_scope.
+#[local] Definition R := Rdefinitions.R.
+
+Import Order.Theory GRing.Theory Num.Theory.
 
 Section joint_typ_seq_definition.
 
 Variables A B : finType.
-Variable P : R.-fdist A.
+Variable P : {fdist A}.
 Variable W : `Ch(A, B).
 Variable n : nat.
 Variable epsilon : R.
@@ -63,19 +65,13 @@ Definition set_jtyp_seq : {set 'rV[A * B]_n} := [set tab | jtyp_seq tab].
 Local Notation "'`JTS'" := (set_jtyp_seq).
 
 Lemma typical_sequence1_JTS x : prod_rV x \in `JTS ->
-  exp2 (- INR n * (`H P + epsilon)) <= P `^ n x.1 <= exp2 (- INR n * (`H P - epsilon)).
-Proof.
-rewrite inE => /and3P[/andP[/RleP JTS11 /RleP JTS12] _ _].
-by rewrite prod_rVK in JTS11, JTS12.
-Qed.
+  Exp 2 (- n%:R * (`H P + epsilon)) <= (P `^ n) x.1 <= Exp 2 (- n%:R * (`H P - epsilon)).
+Proof. by rewrite inE /jtyp_seq prod_rVK => /and3P[] /andP[-> ->]. Qed.
 
 Lemma typical_sequence1_JTS' x : prod_rV x \in `JTS ->
-  exp2 (- INR n * (`H (`O( P , W)) + epsilon)) <= (`O( P , W)) `^ n x.2 <=
-  exp2 (- INR n * (`H (`O( P , W)) - epsilon)).
-Proof.
-rewrite inE => /and3P[_ /andP[/RleP JTS11 /RleP JTS12] _].
-by rewrite prod_rVK in JTS11, JTS12.
-Qed.
+  Exp 2 (- n%:R * (`H (`O( P , W)) + epsilon)) <= (`O( P , W) `^ n) x.2 <=
+  Exp 2 (- n%:R * (`H (`O( P , W)) - epsilon)).
+Proof. by rewrite inE /jtyp_seq prod_rVK => /and3P[_] /andP[-> ->]. Qed.
 
 End joint_typ_seq_definition.
 
@@ -88,28 +84,33 @@ Variables (A B : finType) (P : {fdist A}) (W : `Ch(A, B)).
 Variable n : nat.
 Variable epsilon : R.
 
-Lemma JTS_sup : INR #| `JTS P W n epsilon| <= exp2 (INR n * (`H(P , W) + epsilon)).
+Lemma JTS_sup :
+  #| `JTS P W n epsilon|%:R <= Exp 2 (n%:R * (`H(P , W) + epsilon)).
 Proof.
-have : INR #|`JTS P W n epsilon| <= INR #|`TS ((P `X W)) n epsilon|.
+have : #|`JTS P W n epsilon|%:R <= #|`TS ((P `X W)) n epsilon|%:R :> R.
   suff : `JTS P W n epsilon \subset `TS ((P `X W)) n epsilon.
-    by move/subset_leq_card/leP/le_INR.
+    by rewrite ler_nat => /subset_leq_card.
   apply/subsetP => tab.
   by rewrite /set_jtyp_seq inE /jtyp_seq inE => /and3P[].
-move/leR_trans; apply; exact: (@TS_sup _ ((P `X W)) epsilon n).
+move/le_trans; apply; exact: TS_sup.
 Qed.
 
 End jtyp_seq_upper.
 
 Section jtyp_seq_transmitted.
 Variables (A B : finType) (P : {fdist A}) (W : `Ch(A, B)).
 Variable epsilon : R.
-
-Local Open Scope zarith_ext_scope.
+Definition Nup (x : R) := `| Num.floor x |.+1.
+Lemma Nup_gt x : x < (Nup x)%:R.
+Proof.
+apply: (lt_le_trans (lt_succ_floor x)).
+by rewrite /Nup -intrD1 -natr1 lerD // natr_absz ler_int ler_norm.
+Qed.
 
 Definition JTS_1_bound :=
-  maxn '| up (aep_bound P (epsilon / 3)) |
- (maxn '| up (aep_bound (`O(P , W)) (epsilon / 3)) |
-       '| up (aep_bound ((P `X W)) (epsilon / 3)) |).
+  maxn (Nup (aep_bound P (epsilon / 3)))
+ (maxn (Nup (aep_bound (`O(P , W)) (epsilon / 3)))
+       (Nup (aep_bound ((P `X W)) (epsilon / 3)))).
 
 Variable n : nat.
 Hypothesis He : 0 < epsilon.
@@ -118,120 +119,98 @@ Lemma JTS_1 : (JTS_1_bound <= n)%nat ->
   1 - epsilon <= Pr ((P `X W) `^ n) (`JTS P W n epsilon).
 Proof.
 have : (JTS_1_bound <= n)%nat ->
-  Pr ( (P `^ n `X (W ``^ n)) )
+  Pr ( ((P `^ n) `X (W ``^ n)) )
     [set x | x.1 \notin `TS P n epsilon] +
-  Pr ( (P `^ n `X (W ``^ n)) )
+  Pr ( ((P `^ n) `X (W ``^ n)) )
     [set x | x.2 \notin `TS (`O(P , W)) n epsilon] +
-  Pr ( (P `^ n `X  (W ``^ n)))
+  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.
+    move: (set_typ_seq_incl P m (ltW He)) => Hincl.
     rewrite (Pr_DMC_fst P W (fun x => x \notin `TS P m epsilon)).
     apply/subset_Pr/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 ->
+  have {H1}HnP : forall n, (Nup (aep_bound P (epsilon / 3)) <= n)%N ->
     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].
+    apply: le_trans; first exact: (H1 m).
+    have m_prednK : m.-1.+1 = m by rewrite prednK // (leq_trans _ Hm).
     have : 1 - (epsilon / 3) <= Pr (P `^ m) (`TS P m (epsilon/3)).
       rewrite -m_prednK.
-      apply Pr_TS_1.
-      - by apply divR_gt0 => //; lra.
+      apply: Pr_TS_1.
+      - by rewrite divr_gt0.
       - 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.
+        move: Hm; rewrite -(ler_nat R); exact/le_trans/ltW/Nup_gt.
+    rewrite lerBlDr addrC -lerBlDr; apply: le_trans.
+    by rewrite Pr_to_cplt setCK.
   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.
+    have Hincl := set_typ_seq_incl (`O(P , W)) m (ltW He).
     rewrite Pr_DMC_out.
     apply/subset_Pr/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 ->
+  have {H1}HnPW m : (Nup (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 (* TODO: ssrZ? *); split; [by []|apply/up_pos/aep_bound_ge0; lra].
+    apply: le_trans; first exact: (H1 m).
+    have m_prednK : m.-1.+1 = m by rewrite prednK // (leq_trans _ Hm).
     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.
+      apply: Pr_TS_1.
+      - by rewrite divr_gt0.
+      - move: Hm.
+        rewrite m_prednK -(ler_nat R).
+        exact/le_trans/ltW/Nup_gt.
+    rewrite lerBlDr addrC -lerBlDr; apply: le_trans.
+    by rewrite Pr_to_cplt setCK.
   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.
+    have Hincl := set_typ_seq_incl ((P `X W)) m (ltW He).
     apply/subset_Pr/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 ->
+  have {H1}HnP_W m : (Nup (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].
+    apply: le_trans; first exact: (H1 m).
+    have m_prednK : m.-1.+1 = m by rewrite prednK // (leq_trans _ Hm).
     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.
+      rewrite -m_prednK; apply: Pr_TS_1.
+      - by rewrite divr_gt0.
+      - move: Hm; rewrite m_prednK -(ler_nat R).
+        exact/le_trans/ltW/Nup_gt.
+    rewrite lerBlDr addrC -lerBlDr; apply: le_trans.
+    by rewrite Pr_to_cplt setCK.
   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.
+  apply lerD; first by apply lerD; [exact: HnP | exact: HnPW].
+  apply: le_trans; last exact/HnP_W/Hn3.
+  by apply/eqW; congr Pr; apply/setP => /= tab; 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 (
+  by rewrite lerBlDr lerD2l.
+apply (@le_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/eqW; congr Pr; apply/setP => xy;  rewrite !inE 2!negb_and orbA.
+apply: le_trans; last exact: Hn_Pr.
+apply (@le_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: le_Pr_setU.
-rewrite -addRA !Pr_DMC_rV_prod; apply/leR_add2l; apply: leR_trans (le_Pr_setU _ _ _).
-by apply/Req_le; congr Pr; apply/setP => t; rewrite !inE rV_prodK.
+rewrite -addrA !Pr_DMC_rV_prod lerD2l //; apply: le_trans (le_Pr_setU _ _ _).
+by apply/eqW; congr Pr; apply/setP => t; rewrite !inE rV_prodK.
 Qed.
 
 End jtyp_seq_transmitted.
@@ -240,30 +219,30 @@ Section non_typicality.
 Variables (A B : finType) (P : {fdist A}) (W : `Ch(A, B)) (n : nat) (epsilon : R).
 
 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)).
+  [set x | prod_rV x \in `JTS P W n epsilon] <= Exp 2 (- n%:R * (`I(P, W) - 3 * epsilon)).
 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))))) => /=.
+apply (@le_trans _ _ (\sum_(i | i \in `JTS P W n epsilon)
+    (Exp 2 (- n%:R * (`H P - epsilon)) * Exp 2 (- 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.
+  - rewrite fdist_prodE ler_pM //.
+      by case/andP: (typical_sequence1_JTS iJTS).
+    by case/andP: (typical_sequence1_JTS' iJTS).
+  - by rewrite mulr_ge0 // Exp_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.
+  #| `JTS P W n epsilon|%:R *
+  Exp 2 (- n%:R * (`H P - epsilon)) * Exp 2 (- n%:R * (`H( P `o W) - epsilon)));
+  last by rewrite big_const iter_addr addr0 -mulr_natl mulrA.
+apply (@le_trans _ _ (Exp 2 (n%:R * (`H( P , W ) + epsilon)) *
+  Exp 2 (- n%:R * (`H P - epsilon)) * Exp 2 (- n%:R * (`H( P `o W ) - epsilon)))).
+  by rewrite !ler_wpM2r ?Exp_ge0 // JTS_sup.
+apply/eqW.
+rewrite /Exp -!exp.powRD; try by rewrite (@eqr_nat R 2 0) implybT.
+rewrite /mutual_info_chan !mulrDr !mulrNN; congr exp.powR.
+by rewrite (_ : 3 * epsilon = epsilon + epsilon + epsilon) //; field.
 Qed.
 
 End non_typicality.