Exp cleaning (wip)

affeldt-aist · Jan 31, 2025 · 59b2626 · 59b2626
1 parent 5fab5db
commit 59b2626
Show file tree

Hide file tree

Showing 13 changed files with 191 additions and 265 deletions.
diff --git a/information_theory/channel_coding_converse.v b/information_theory/channel_coding_converse.v
@@ -64,11 +64,9 @@ apply ler_wpM2l.
   by rewrite exprn_ge0//.
 set Vmax := [arg max_(V > _) _]%O.
 rewrite /success_factor_bound /exp_cdiv.
-case : ifP => Hcase; last first.
-  by rewrite mul0r Exp_ge0.
-rewrite -exp.powRD; last first.
-  by rewrite pnatr_eq0 implybT.
-rewrite exp.ler_powR ?ler1n//.
+case : ifP => Hcase; last by rewrite mul0r powR_ge0.
+rewrite -powRD; last by rewrite pnatr_eq0 implybT.
+rewrite ler_powR ?ler1n//.
 rewrite -mulrDr 2!mulNr.
 rewrite lerNr opprK; apply/ler_wpM2l; first exact/ler0n.
 have {}Hcase : Pmax |- Vmax << W.
@@ -105,7 +103,7 @@ Theorem channel_coding_converse : exists n0,
 Proof.
 case: (channel_coding_converse_gen minRate_cap set_of_I_has_ubound) => Delta [Delta_pos HDelta].
 pose K := (#|A| + #|A| * #|B|)%nat.
-pose n0 := 2 ^+ K * K.+1`!%:R / ((Delta * exp.ln 2) ^+ K.+1) / epsilon.
+pose n0 := 2 ^+ K * K.+1`!%:R / ((Delta * ln 2) ^+ K.+1) / epsilon.
 exists n0 => n M c HM n0_n HminRate.
 have Rlt0n : 0 < n%:R :> R.
   apply: (lt_trans _ n0_n).
@@ -114,7 +112,7 @@ have Rlt0n : 0 < n%:R :> R.
   rewrite -mulrA mulr_gt0 ?exprn_gt0//.
   rewrite divr_gt0// ?ltr0n ?fact_gt0//.
   rewrite exprn_gt0//.
-  by rewrite mulr_gt0// exp.ln_gt0// ltr1n.
+  by rewrite mulr_gt0// ln_gt0// ltr1n.
 destruct n as [|n'].
   by rewrite ltxx in Rlt0n.
 set n := n'.+1.
@@ -134,19 +132,19 @@ rewrite -2!mulrA.
 set aux := _%:R * (_ * _).
 have aux_gt0 : 0 < aux.
   rewrite mulr_gt0 ?ltr0n ?fact_gt0// divr_gt0//.
-  by rewrite invr_gt0// exprn_gt0// mulr_gt0// exp.ln_gt0 ?ltr1n.
+  by rewrite invr_gt0// exprn_gt0// mulr_gt0// ln_gt0 ?ltr1n.
 apply (@le_trans _ _ ((n.+1%:R / n%:R) ^+ K * aux)); last first.
   rewrite ler_pM2r//.
   rewrite lerXn2r ?nnegrE ?divr_ge0//.
   rewrite ler_pdivrMr ?ltr0n//.
   by rewrite -[in leRHS]mulrC mulr_natr mulr2n -natr1 lerD2l ler1n.
 rewrite expr_div_n -mulrA ler_wpM2l//.
 - by rewrite exprn_ge0.
-- rewrite -lef_pV2 ?posrE ?Exp_gt0//; last first.
+- rewrite -lef_pV2 ?posrE ?powR_gt0//; last first.
     by rewrite mulr_gt0// invr_gt0 exprn_gt0.
   rewrite -powRN mulNr opprK.
-  have nDeltaln2 : 0 < n%:R * Delta * exp.ln 2.
-    by rewrite mulr_gt0// ?exp.ln_gt0 ?ltr1n// mulr_gt0//.
+  have nDeltaln2 : 0 < n%:R * Delta * ln 2.
+    by rewrite mulr_gt0// ?ln_gt0 ?ltr1n// mulr_gt0//.
   rewrite /exp.powR(* TODO *) pnatr_eq0/=.
   apply/ltW.
   apply: (le_lt_trans _ (exp_strict_lb K.+1 nDeltaln2)) => {nDeltaln2}.

diff --git a/information_theory/channel_coding_direct.v b/information_theory/channel_coding_direct.v
@@ -28,8 +28,8 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Import Prenex Implicits.
 
-Local Open Scope ring_scope.
 Local Open Scope fdist_scope.
+Local Open Scope ring_scope.
 Local Open Scope jtyp_seq_scope.
 Local Open Scope channel_code_scope.
 Local Open Scope channel_scope.
@@ -49,9 +49,9 @@ Lemma f0 g : 0 <= f g. Proof. by rewrite ffunE prodr_ge0. Qed.
 Lemma f1 : \sum_(g in {ffun M -> 'rV[A]_n}) f g = 1.
 Proof.
 under eq_bigr do rewrite ffunE /=.
-rewrite -(bigA_distr_bigA (fun _ v => (P `^ n) v)) /=.
+rewrite -(bigA_distr_bigA (fun _ => (P `^ n)%fdist)) /=.
 rewrite [RHS](_ : _ = \prod_(m0 : M | xpredT m0) 1); last by rewrite big1.
-by apply eq_bigr => _ _; rewrite (FDist.f1 (P `^ n)).
+by apply eq_bigr => _ _; rewrite (FDist.f1 (P `^ n)%fdist).
 Qed.
 
 Definition d : {fdist encT A M n} := locked (FDist.make f0 f1).
@@ -253,7 +253,7 @@ Definition epsilon0_condition r epsilon epsilon0 :=
 Definition frac_part (x : R) := x - (Num.floor x)%:~R.
 Definition n_condition r epsilon0 n :=
   (O < n)%nat /\ - log epsilon0 / epsilon0 < n%:R /\
-  frac_part (2 `^ (r *+ n))%R = 0 /\ (JTS_1_bound P W epsilon0 <= n)%nat.
+  frac_part (2 `^ (r *+ n)) = 0 /\ (JTS_1_bound P W epsilon0 <= n)%nat.
 
 Definition cal_E M n epsilon (f : encT A M n) m :=
   [set vb | prod_rV (f m, vb) \in `JTS P W n epsilon].
@@ -294,7 +294,7 @@ transitivity (\sum_(j : {ffun 'I_k -> 'rV[_]_n}) \prod_(m < k) (Q `^ _)%fdist (j
   - move=> i /=; apply/esym/eqP/eq_from_tnth => j.
     by rewrite tnth_fgraph ffunE enum_valK.
   - by move=> i _; apply eq_bigr => j _; rewrite ffunE /= tcastE -enum_rank_ord.
-rewrite -(bigA_distr_bigA (fun m xn => (Q `^ _) xn)) /= big_const.
+rewrite -(bigA_distr_bigA (fun _ => (Q `^ _)%fdist)) /= big_const.
 by rewrite FDist.f1 iter_mulr mulr1 expr1n.
 Qed.
 
@@ -686,14 +686,12 @@ have [k Hk] : exists k, log k.+1%:R / n%:R = r :> R.
   rewrite prednK; last first.
     rewrite absz_gt0; apply/eqP => Habs.
     rewrite /frac_part Habs subr0 in Hn2.
-    suff : false => //.
-    have := @Exp_gt0 R 2 (rate r *+ n).
-    by rewrite Hn2 ltxx; apply.
+    by move/eqP : Hn2; apply/negP; rewrite gt_eqF// powR_gt0.
   rewrite eqr_divr_mulr; last by rewrite (eqr_nat R n 0) -lt0n.
   rewrite -[in LHS]mulrz_nat natz gez0_abs.
     move/subr0_eq: Hn2 => <-.
     by rewrite /log ExpK // mulr_natr.
-  by rewrite floor_ge0 Exp_ge0.
+  by rewrite floor_ge0 powR_ge0.
 set M : finType := 'I_k.+1.
 exists M.
 split; first by rewrite /= card_ord.
@@ -779,7 +777,7 @@ rewrite (_ : _ + _ = - n%:R * (`I(P, W) - log #| M |%:R / n%:R - 3 * epsilon0));
   by case: Hn; rewrite -(ltr_nat R) => /lt0r_neq0.
 rewrite (_ : _ / _ = rate r); last by rewrite -Hk card_ord.
 apply (@lt_trans _ _ (2 `^ (- n%:R * epsilon0))).
-  apply Exp_increasing; first by rewrite (ltr_nat R 1 2).
+  rewrite gt1_ltr_powRr ?ltr1n//.
   rewrite -mulr_natr -mulNr.
   rewrite -2!mulrA ltr_nM2l ?oppr_lt0 //.
   rewrite ltr_pM2l; last by case: Hn; rewrite (ltr_nat R 0 n).
@@ -807,7 +805,7 @@ Lemma exists_frac_part (P : nat -> Prop) : (exists n, P n) ->
   forall num den, (0 < num)%nat -> (0 < den)%nat ->
   (forall n m, (n <= m)%nat -> P n -> P m) ->
   exists n, P n /\
-    frac_part (2 `^ (n%:R * (log num%:R / den%:R)))%R = 0.
+    frac_part (2 `^ (n%:R * (log num%:R / den%:R))) = 0.
 Proof.
 case=> n Pn num den Hden HP.
 exists (n * den)%nat.
@@ -816,7 +814,7 @@ split.
   by rewrite -{1}(muln1 n) leq_mul2l HP orbC.
 rewrite natrM -mulrA (mulrCA den%:R) mulrV // ?mulr1; last first.
   by rewrite unitfE lt0r_neq0 // (ltr_nat R 0).
-rewrite /frac_part mulrC exp.powRrM -/(2 `^ _)%R.
+rewrite /frac_part mulrC powRrM.
 rewrite (LogK (n:=2)) // ?ltr0n // powR_mulrn ?ler0n // -natrX.
 by rewrite floorK ?subrr // intr_nat.
 Qed.
@@ -891,7 +889,7 @@ case: (random_coding_good_code He Hepsilon0 Hn) =>
 case: (good_code_sufficient_condition H) => f Hf.
 exists n, M, (mkCode f (jtdec P W epsilon0 f)); split => //.
 rewrite /CodeRate M_k -mulrz_nat natz gez0_abs; last first.
-  by rewrite floor_ge0 Exp_ge0.
+  by rewrite floor_ge0 powR_ge0.
 case: Hn => Hn [_] [].
 rewrite /frac_part => /subr0_eq <- _.
 rewrite /log ExpK // -(mulr_natr (rate r)) mulrK //.

diff --git a/information_theory/conditional_divergence.v b/information_theory/conditional_divergence.v
@@ -20,8 +20,8 @@ Unset Strict Implicit.
 Import Prenex Implicits.
 
 Local Open Scope reals_ext_scope.
-Local Open Scope ring_scope.
 Local Open Scope fdist_scope.
+Local Open Scope ring_scope.
 Local Open Scope entropy_scope.
 Local Open Scope channel_scope.
 Local Open Scope divergence_scope.
@@ -33,7 +33,7 @@ Import Order.TTheory GRing.Theory Num.Theory.
 Section conditional_dominance.
 Variables (A B : finType) (V W : `Ch(A, B)) (P : {fdist A}).
 
-Definition cdom_by := forall a, P a != 0%R -> V a `<< W a.
+Definition cdom_by := forall a, P a != 0 -> V a `<< W a.
 
 Lemma dom_by_cdom_by : (P `X V) `<< (P `X W) <-> cdom_by.
 Proof.
@@ -178,8 +178,7 @@ transitivity (\prod_(a : A) \prod_(b : B) \prod_(i < n)
 apply eq_bigr => a _; apply eq_bigr => b _.
 rewrite num_co_occ_alt -sum1_card.
 rewrite (@big_morph _ _ (fun x => W a b ^+ x) 1 *%R O addn) //; last first.
-  move=> * /=.
-  by rewrite exprD.
+  by move=> * /=; rewrite exprD.
 rewrite [in RHS]big_mkcond.
 apply eq_bigr => i _.
 case: ifP.
@@ -204,7 +203,7 @@ Hypothesis Hn : n != O.
    the conditional divergence and the condition entropy *)
 
 Lemma dmc_cdiv_cond_entropy :
-  (W ``(y | x) = 2 `^ (- n%:R * (D(V || W | P) + `H(V | P))))%R.
+  W ``(y | x) = 2 `^ (- n%:R * (D(V || W | P) + `H(V | P))).
 Proof.
 rewrite dmc_cdiv_cond_entropy_aux cond_entropy_chanE2.
 rewrite /cdiv /entropy -big_split /=.
@@ -239,17 +238,13 @@ case/boolP : (V a b == 0) => [/eqP|] Vab0.
     by rewrite expr0 Vab0 !(mulr0,mul0r,addr0,add0r,oppr0,powRr0).
   move: Hy; rewrite in_set => /forallP/(_ a)/forallP/(_ b)/eqP => ->.
   by rewrite jtype_0_jtypef.
-rewrite -exp.powR_mulrn ?Exp_ge0//.
-rewrite -exp.powRrM//.
-congr (exp.powR _ _).
-(*rewrite -exp2_pow; congr exp2.*)
+rewrite -powR_mulrn ?powR_ge0// -powRrM//.
+congr (_ `^ _).
 rewrite -mulrN -mulrDr mulrA.
 rewrite logM; last 2 first.
   by rewrite -fdist_gt0.
-  rewrite invr_gt0.
-  by rewrite -fdist_gt0.
-rewrite logV; last first.
-  by rewrite -fdist_gt0.
+  by rewrite invr_gt0 -fdist_gt0.
+rewrite logV; last by rewrite -fdist_gt0.
 rewrite addrAC subrr add0r.
 rewrite mulrN 3!mulNr opprK.
 rewrite mulrC.
@@ -277,17 +272,20 @@ Variable W : `Ch*(A, B).
 
 Definition exp_cdiv :=
   if (type.d P) |- V <<b W
-  then (2 `^ (- n%:R * D(V || W | P)))%R
+  then 2 `^ (- n%:R * D(V || W | P))
   else 0.
 
-Lemma exp_cdiv_left (H : P |- V << W) : (exp_cdiv = 2 `^ (- n%:R * D(V || W | P)))%R.
+Lemma exp_cdiv_left (H : P |- V << W) : exp_cdiv = 2 `^ (- n%:R * D(V || W | P)).
 Proof.
 rewrite /exp_cdiv.
 suff : (type.d P) |- V <<b W by move=> ->.
 apply/forallP => a; apply/implyP => Pa0.
-apply/forall_inP => b /eqP Wab; by rewrite (dominatesE (H _ Pa0)).
+by apply/forall_inP => b /eqP Wab; rewrite (dominatesE (H _ Pa0)).
 Qed.
 
+Lemma exp_cdiv_ge0 : 0 <= exp_cdiv.
+Proof. by rewrite /exp_cdiv; case: ifPn => // _; rewrite powR_ge0. Qed.
+
 End cdiv_specialized.
 
 Section dmc_cdiv_cond_entropy_spec.
@@ -308,8 +306,7 @@ Lemma dmc_exp_cdiv_cond_entropy :
 Proof.
 rewrite /exp_cdiv.
 case : ifP => Hcase.
-- rewrite -exp.powRD; last first.
-   by rewrite pnatr_eq0 implybT.
+- rewrite -powRD; last by rewrite pnatr_eq0 implybT.
   rewrite -mulrDr.
   apply dmc_cdiv_cond_entropy => //.
   (* TODO: lemma? *)

diff --git a/information_theory/joint_typ_seq.v b/information_theory/joint_typ_seq.v
@@ -189,7 +189,7 @@ have : (JTS_1_bound <= n)%nat ->
     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.
+  rewrite [in X in _ <= X](_ : epsilon = epsilon / 3 + epsilon / 3 + epsilon / 3); last by field.
   move: Hn; rewrite 2!geq_max => /andP[Hn1 /andP[Hn2 Hn3]].
   rewrite !Pr_DMC_rV_prod.
   apply lerD; first by apply lerD; [exact: HnP | exact: HnPW].
@@ -231,15 +231,15 @@ apply (@le_trans _ _ (\sum_(i | i \in `JTS P W n epsilon)
   - 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 mulr_ge0 ?powR_ge0.
   - by rewrite prod_rVK eqxx andbC.
 rewrite (_ : \sum_(_ | _) _ =
   #| `JTS P W n epsilon|%:R *
   2 `^ (- n%:R * (`H P - epsilon)) * 2 `^ (- n%:R * (`H( P `o W) - epsilon)));
   last by rewrite big_const iter_addr addr0 -mulr_natl mulrA.
 apply (@le_trans _ _ (2 `^ (n%:R * (`H( P , W ) + epsilon)) *
   2 `^ (- n%:R * (`H P - epsilon)) * 2 `^ (- n%:R * (`H( P `o W ) - epsilon)))).
-  by rewrite !ler_wpM2r ?Exp_ge0 // JTS_sup.
+  by rewrite !ler_wpM2r ?powR_ge0 // JTS_sup.
 apply/eqW.
 rewrite -!powRD; try by rewrite (@eqr_nat R 2 0) implybT.
 rewrite /mutual_info_chan !mulrDr !mulrNN; congr exp.powR.