From b59add2f9769f51509125ec9cc126b16a0a594b9 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Fri, 4 Oct 2024 17:15:11 +0900 Subject: [PATCH] shannon-fano --- information_theory/aep.v | 93 ++++++------ information_theory/binary_symmetric_channel.v | 138 +++++++++--------- information_theory/shannon_fano.v | 76 +++++----- lib/binary_entropy_function.v | 31 ++-- lib/logb.v | 1 - lib/realType_ext.v | 68 +++++++++ lib/realType_logb.v | 51 +++++++ 7 files changed, 286 insertions(+), 172 deletions(-) diff --git a/information_theory/aep.v b/information_theory/aep.v index cfa6708a..3ce518d0 100644 --- a/information_theory/aep.v +++ b/information_theory/aep.v @@ -2,9 +2,8 @@ (* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later *) From mathcomp Require Import all_ssreflect ssralg ssrnum matrix. From mathcomp Require boolp. -Require Import Reals. -From mathcomp Require Import Rstruct. -Require Import ssrR Reals_ext realType_ext ssr_ext bigop_ext ssralg_ext logb. +From mathcomp Require Import reals exp Rstruct. +Require Import realType_ext ssr_ext bigop_ext ssralg_ext realType_logb. Require Import fdist proba entropy. (******************************************************************************) @@ -26,48 +25,48 @@ Local Open Scope entropy_scope. Local Open Scope ring_scope. Local Open Scope vec_ext_scope. +Import Order.POrderTheory GRing.Theory Num.Theory. + Section mlog_prop. Variables (A : finType) (P : {fdist A}). -Local Open Scope R_scope. -Definition aep_sigma2 := `E ((`-- (`log P)) `^2) - (`H P)^2. +Definition aep_sigma2 : Rdefinitions.R := `E ((`-- (`log P)) `^2) - (`H P)^+2. -Lemma aep_sigma2E : aep_sigma2 = \sum_(a in A) P a * (log (P a))^2 - (`H P)^2. +Lemma aep_sigma2E : aep_sigma2 = \sum_(a in A) P a * (log (P a))^+2 - (`H P)^+2. Proof. rewrite /aep_sigma2 /Ex [in LHS]/log_RV /sq_RV /comp_RV. -by under eq_bigr do rewrite mulRC /ambient_dist -mulRR Rmult_opp_opp mulRR. +by under eq_bigr do rewrite mulrC /ambient_dist expr2 mulrNN -expr2. Qed. Lemma V_mlog : `V (`-- (`log P)) = aep_sigma2. Proof. rewrite aep_sigma2E /Var E_trans_RV_id_rem -entropy_Ex. transitivity - (\sum_(a in A) ((- log (P a))^2 * P a - 2 * `H P * - log (P a) * P a + - `H P ^ 2 * P a))%R. + (\sum_(a in A) ((- log (P a))^+2 * P a - 2 * `H P * - log (P a) * P a + + `H P ^+ 2 * P a))%R. apply eq_bigr => a _. rewrite /scalel_RV /log_RV /neg_RV /trans_add_RV /sq_RV /comp_RV /= /sub_RV. - by rewrite /ambient_dist; field. -rewrite big_split /= big_split /= -big_distrr /= (FDist.f1 P) mulR1. -rewrite (_ : \sum_(a in A) - _ = - (2 * `H P ^ 2))%R; last first. - rewrite -{1}big_morph_oppR; congr (- _)%R. + by rewrite /ambient_dist -!mulrBl -mulrDl. +rewrite big_split /= big_split /= -big_distrr /= (FDist.f1 P) mulr1. +rewrite (_ : \sum_(a in A) - _ = - (2 * `H P ^+ 2))%R; last first. + rewrite -{1}big_morph_oppr; congr (- _)%R. rewrite [X in X = _](_ : _ = \sum_(a in A) (2 * `H P) * (- (P a * log (P a))))%R; last first. - by apply eq_bigr => a _; rewrite -!mulRA (mulRC (P a)) mulNR. - rewrite -big_distrr [in LHS]/= -{1}big_morph_oppR. - by rewrite -/(entropy P) -mulRA /= mulR1. + by apply eq_bigr => a _; rewrite (mulrC (P a)) -[in RHS]mulNr mulrA. + rewrite -big_distrr [in LHS]/= -{1}big_morph_oppr. + by rewrite -/(entropy P) expr2 mulrA. set s := ((\sum_(a in A ) _)%R in LHS). -rewrite (_ : \sum_(a in A) _ = s)%R; last by apply eq_bigr => a _; field. -rewrite RpowE GRing.expr2 -!RmultE mulR1. -field. +rewrite (_ : \sum_(a in A) _ = s)%R; last first. + by apply eq_bigr => a _; rewrite sqrrN mulrC. +by rewrite (mulr_natl _ 2) mulr2n opprD addrA subrK. Qed. Lemma aep_sigma2_ge0 : 0 <= aep_sigma2. -Proof. rewrite -V_mlog /Var; apply Ex_ge0 => ?; exact: pow_even_ge0. Qed. - +Proof. by rewrite -V_mlog /Var; apply: Ex_ge0 => ?; exact: sq_RV_ge0. Qed. End mlog_prop. -Definition sum_mlog_prod (A : finType) (P : {fdist A}) n : {RV (P `^ n) -> R} := - (fun t => \sum_(i < n) - log (P t ``_ i))%R. +Definition sum_mlog_prod (A : finType) (P : {fdist A}) n : {RV ((P `^ n)%fdist)-> Rdefinitions.R} := + (fun t => \sum_(i < n) - log (P (t ``_ i)))%R. Arguments sum_mlog_prod {A} _ _. @@ -75,13 +74,13 @@ Lemma sum_mlog_prod_sum_map_mlog (A : finType) (P : {fdist A}) n : sum_mlog_prod P n.+1 \=sum (\row_(i < n.+1) `-- (`log P)). Proof. elim : n => [|n IH]. -- move: (@sum_n_1 A P (\row_i `-- (`log P))). +- move: (@sum_n_1 _ A P (\row_i `-- (`log P))). set mlogP := cast_fun_rV10 _. move => HmlogP. set mlogprodP := @sum_mlog_prod _ _ 1. suff -> : mlogprodP = mlogP by []. rewrite /mlogprodP /mlogP /sum_mlog_prod /cast_fun_rV10 /= mxE /=. - by rewrite boolp.funeqE => ta; rewrite big_ord_recl big_ord0 addR0. + by rewrite boolp.funeqE => ta; rewrite big_ord_recl big_ord0 addr0. - rewrite [X in _ \=sum X](_ : _ = row_mx (\row_(i < 1) (`-- (`log P))) (\row_(i < n.+1) `-- (`log P))); last first. apply/rowP => b; rewrite !mxE; case: splitP. @@ -96,52 +95,52 @@ Section aep_k0_constant. Local Open Scope R_scope. Variables (A : finType) (P : {fdist A}). -Definition aep_bound epsilon := (aep_sigma2 P / epsilon ^ 3)%R. +Definition aep_bound epsilon : Rdefinitions.R := (aep_sigma2 P / epsilon ^+ 3)%R. Lemma aep_bound_ge0 e (_ : 0 < e) : 0 <= aep_bound e. -Proof. apply divR_ge0; [exact: aep_sigma2_ge0 | exact/pow_lt]. Qed. +Proof. by apply divr_ge0; [exact: aep_sigma2_ge0 | apply/exprn_ge0/ltW]. Qed. Lemma aep_bound_decreasing e e' : 0 < e' <= e -> aep_bound e <= aep_bound e'. Proof. -case=> Oe' e'e. -apply leR_wpmul2l; first exact: aep_sigma2_ge0. -apply leR_inv => //; first exact/pow_lt. -apply pow_incr => //; split; [exact/ltRW | exact/e'e ]. +case/andP=> Oe' e'e. +apply ler_wpM2l; first exact: aep_sigma2_ge0. +rewrite lef_pV2 ?posrE; [|apply/exprn_gt0..] => //; last first. + by rewrite (lt_le_trans _ e'e). +by rewrite lerXn2r// ?nnegrE ltW// (lt_le_trans _ e'e). Qed. End aep_k0_constant. - Section AEP. Local Open Scope R_scope. -Variables (A : finType) (P : {fdist A}) (n : nat) (epsilon : R). +Variables (A : finType) (P : {fdist A}) (n : nat) (epsilon : Rdefinitions.R). Hypothesis Hepsilon : 0 < epsilon. Lemma aep : aep_bound P epsilon <= n.+1%:R -> - Pr (P `^ n.+1) [set t | (0 < P `^ n.+1 t)%mcR && - (`| (`-- (`log (P `^ n.+1)) `/ n.+1) t - `H P | >= epsilon)%mcR ] <= epsilon. + Pr (P `^ n.+1)%fdist [set t | (0 < (P `^ n.+1)%fdist t) && + (`| (`-- (`log (P `^ n.+1)%fdist) `/ n.+1) t - `H P | >= epsilon)%mcR ] <= epsilon. Proof. move=> Hbound. -apply (@leR_trans (aep_sigma2 P / (n.+1%:R * epsilon ^ 2))); last first. +apply (@le_trans _ _ (aep_sigma2 P / (n.+1%:R * epsilon ^+ 2))); last first. rewrite /aep_bound in Hbound. - apply (@leR_wpmul2r (epsilon / n.+1%:R)) in Hbound; last first. - apply divR_ge0; [exact/ltRW/Hepsilon | exact/ltR0n]. - rewrite [in X in _ <= X]mulRCA mulRV ?INR_eq0' // ?mulR1 in Hbound. - apply/(leR_trans _ Hbound)/Req_le; field. - by split; [by rewrite INR_eq0 | exact/eqP/gtR_eqF]. + apply (@ler_wpmul2r _ (epsilon / n.+1%:R)) in Hbound; last first. + by rewrite divr_ge0// ltW. + rewrite [in X in _ <= X]mulrCA mulfV ?pnatr_eq0// ?mulr1 in Hbound. + apply/(le_trans _ Hbound). + rewrite [in leRHS]mulrA [in leRHS]exprSr [in leRHS]invfM. + rewrite -3![in leRHS]mulrA (mulrA epsilon^-1) mulVf ?gt_eqF// mul1r. + by rewrite (mulrC (n.+1%:R)) invfM. have Hsum := sum_mlog_prod_sum_map_mlog P n. have H1 k i : `E ((\row_(i < k.+1) `-- (`log P)) ``_ i) = `H P. by rewrite mxE entropy_Ex. have H2 k i : `V ((\row_(i < k.+1) `-- (`log P)) ``_ i) = aep_sigma2 P. by rewrite mxE V_mlog. have {H1 H2} := (wlln (H1 n) (H2 n) Hsum Hepsilon). -move/(leR_trans _); apply. +move/(le_trans _); apply. apply/subset_Pr/subsetP => ta; rewrite 2!inE => /andP[H1]. -rewrite /sum_mlog_prod [`-- (`log _)]lock /= -lock /= /scalel_RV /log_RV /neg_RV. -rewrite fdist_rVE. -rewrite log_prodR_sumR_mlog //. -move=> i; apply/RltP. -move: i; apply/prod_gt0_inv. +rewrite /sum_mlog_prod [`-- (`log _)]lock /= -lock /scalel_RV /log_RV /neg_RV/=. +rewrite fdist_rVE log_prodr_sumr_mlog //. +apply/prod_gt0_inv. by move=> x; exact: FDist.ge0. by move: H1; rewrite fdist_rVE. Qed. diff --git a/information_theory/binary_symmetric_channel.v b/information_theory/binary_symmetric_channel.v index 29637710..b9da0ca4 100644 --- a/information_theory/binary_symmetric_channel.v +++ b/information_theory/binary_symmetric_channel.v @@ -2,8 +2,7 @@ (* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later *) From mathcomp Require Import all_ssreflect ssralg ssrnum zmodp matrix lra. From mathcomp Require Import mathcomp_extra classical_sets Rstruct reals. -Require Import Reals Lra. -Require Import ssrR Reals_ext realType_ext logb ssr_ext ssralg_ext bigop_ext. +Require Import realType_ext realType_logb ssr_ext ssralg_ext bigop_ext. Require Import fdist entropy binary_entropy_function channel hamming channel_code. Require Import pproba. @@ -22,13 +21,13 @@ Import Prenex Implicits. Local Open Scope fdist_scope. Local Open Scope channel_scope. -Local Open Scope R_scope. +Local Open Scope ring_scope. Module BSC. Section BSC_sect. Variable A : finType. Hypothesis card_A : #|A| = 2%nat. -Variable p : {prob R}. +Variable p : {prob Rdefinitions.R}. Definition c : `Ch(A, A) := fdist_binary card_A p. @@ -42,66 +41,64 @@ Import Order.TTheory GRing.Theory Num.Def Num.Theory. Section bsc_capacity_proof. Variable A : finType. Hypothesis card_A : #|A| = 2%nat. -Variables (P : {fdist A}) (p : R). +Variables (P : {fdist A}) (p : Rdefinitions.R). Hypothesis p_01' : (0 < p < 1)%mcR. Let p_01'_ : (0 <= p <= 1)%mcR. by move: p_01' => /andP[/ltW -> /ltW ->]. Qed. -Let p_01 : {prob R} := Eval hnf in Prob.mk_ p_01'_. +Let p_01 : {prob Rdefinitions.R} := Eval hnf in Prob.mk_ p_01'_. Lemma HP_HPW : `H P - `H(P, BSC.c card_A p_01) = - H2 p. Proof. rewrite {2}/entropy /=. rewrite (eq_bigr (fun a => ((P `X (BSC.c card_A p_01))) (a.1, a.2) * - log (((P `X (BSC.c card_A p_01))) (a.1, a.2)))); last by case. + log (((P `X (BSC.c card_A p_01))) (a.1, a.2)))); last first. + case=> //=. rewrite -(pair_big xpredT xpredT (fun a b => (P `X (BSC.c card_A p_01)) (a, b) * log ((P `X (BSC.c card_A p_01)) (a, b)))) /=. rewrite {1}/entropy . set a := \sum_(_ in _) _. set b := \sum_(_ <- _) _. -apply trans_eq with (- (a + (-1) * b)); first by field. +apply trans_eq with (- (a + (-1) * b)); first by rewrite mulN1r opprB opprK addrC. rewrite /b {b} big_distrr /= /a {a} -big_split /=. rewrite !Set2sumE /= !fdist_prodE /BSC.c !fdist_binaryxx !fdist_binaryE/=. rewrite eq_sym !(negbTE (Set2.a_neq_b card_A)) /H2 (* TODO *). set a := Set2.a _. set b := Set2.b _. case: (Req_EM_T (P a) 0) => H1. - rewrite H1 !(mul0R, mulR0, addR0, add0R). + rewrite H1 !(mul0r, mulr0, addr0, add0r). move: (FDist.f1 P); rewrite Set2sumE /= -/a -/b. rewrite H1 add0r => ->. - rewrite /log Log_1 -!RmultE !(mul0R, mulR0, addR0, add0R, mul1R, mulR1). - rewrite /onem -RminusE (_ : 1%mcR = 1)//. - field. -rewrite /log LogM; last 2 first. + rewrite log1 !(mul0r, mulr0, addr0, add0r, mul1r, mulr1). + by rewrite /onem mulN1r opprK opprB opprK addrC. +rewrite logM; last 2 first. move/eqP in H1. have [+ _] := fdist_gt0 P a. - by move/(_ H1) => /RltP. - by case/andP: p_01' => ? ?; exact/RltP/onem_gt0. -rewrite /log LogM; last 2 first. + by move/(_ H1). + by case/andP: p_01' => ? ?; exact/onem_gt0. +rewrite logM; last 2 first. move/eqP in H1. have [+ _] := fdist_gt0 P a. - by move/(_ H1) => /RltP. - by case/andP: p_01' => ? ?; exact/RltP. + by move/(_ H1). + by case/andP: p_01'. case: (Req_EM_T (P b) 0) => H2. - rewrite H2 !(mul0R, mulR0, addR0, add0R). + rewrite H2 !(mul0r, mulr0, addr0, add0r). move: (FDist.f1 P); rewrite Set2sumE /= -/a -/b. rewrite H2 addr0 => ->. - rewrite /log Log_1 -!RmultE !(mul0R, mulR0, addR0, add0R, mul1R, mulR1). - rewrite /onem -RminusE (_ : 1%mcR = 1)//. - field. -rewrite /log LogM; last 2 first. + rewrite log1 !(mul0r, mulr0, addr0, add0r, mul1r, mulr1). + rewrite /onem/=. + by rewrite mulN1r opprK opprB opprK addrC. +rewrite logM; last 2 first. move/eqP in H2. have [+ _] := fdist_gt0 P b. - by move/(_ H2) => /RltP. - by case/andP: p_01' => ? ?; exact/RltP. -rewrite /log LogM; last 2 first. + by move/(_ H2). + by case/andP: p_01' => ? ?. +rewrite logM; last 2 first. move/eqP in H2. have [+ _] := fdist_gt0 P b. - by move/(_ H2) => /RltP. - by case/andP: p_01' => ? ?; exact/RltP/onem_gt0. -rewrite /log. -rewrite -!RmultE. -rewrite /onem -RminusE (_ : 1%mcR = 1)//. + by move/(_ H2). + by case/andP: p_01' => ? ?; exact/onem_gt0. +rewrite /onem. transitivity (p * (P a + P b) * log p + (1 - p) * (P a + P b) * log (1 - p) ). rewrite /log. set l2Pa := Log 2 (P a). @@ -110,19 +107,19 @@ transitivity (p * (P a + P b) * log p + (1 - p) * (P a + P b) * log (1 - p) ). set l2p := Log 2 p. set Pa := P a. set Pb := P b. - ring. + lra. move: (FDist.f1 P). rewrite Set2sumE /= -/a -/b. rewrite -RplusE => ->. -rewrite !mulR1. -rewrite /log; field. +rewrite !mulr1. +by rewrite opprB opprK addrC. Qed. Lemma IPW : `I(P, BSC.c card_A p_01) = `H(P `o BSC.c card_A p_01) - H2 p. Proof. -rewrite /mutual_info_chan addRC. +rewrite /mutual_info_chan addrC. set a := `H(_ `o _). -transitivity (a + (`H P - `H(P , BSC.c card_A p_01))); first by field. +transitivity (a + (`H P - `H(P , BSC.c card_A p_01))); first by lra. by rewrite HP_HPW. Qed. @@ -133,51 +130,54 @@ set a := Set2.a _. set b := Set2.b _. rewrite /BSC.c !fdist_binaryxx !fdist_binaryE /= !(eq_sym _ a). rewrite (negbTE (Set2.a_neq_b card_A)). move: (FDist.f1 P); rewrite Set2sumE /= -/a -/b => P1. -rewrite -!(RmultE,RplusE). have -> : p * P a + (1 - p) * P b = 1 - ((1 - p) * P a + p * P b). - rewrite -RplusE (_ : 1%mcR = 1)// in P1. rewrite -{2}P1. - ring_simplify. - congr (_ + _). - by rewrite subRK. -case/andP: p_01' => /RltP Hp1 /RltP Hp2. -rewrite (_ : 0%mcR = 0%coqR)// in Hp1. -rewrite (_ : 1%mcR = 1%coqR)// in Hp2, P1. + set Pa := P a. + set Pb := P b. + lra. +case/andP: p_01' => Hp1 Hp2. have H01 : 0 < ((1 - p) * P a + p * P b) < 1. - move: (FDist.ge0 P a) => /RleP H1. + move: (FDist.ge0 P a) => H1. move: (FDist.le1 P b) => H4. move: (FDist.le1 P a) => H3. - split. - case/Rle_lt_or_eq_dec : H1 => H1; rewrite (_ : 0%mcR = 0)// in H1. - - apply addR_gt0wl. - apply: mulR_gt0 => //. - by rewrite subR_gt0. - apply: mulR_ge0 => //. - exact: ltRW. - - by rewrite -H1 mulR0 add0R (_ : P b = 1) ?mulR1 // -P1 -H1 add0r. + apply/andP; split. + move: H1; rewrite le_eqVlt => /predU1P[H1|H1]; last first. + - apply: ltr_pwDl. + apply: mulr_gt0 => //. + by rewrite subr_gt0. + apply: mulr_ge0 => //. + exact: ltW. + - by rewrite -H1 mulr0 add0r (_ : P b = 1) ?mulr1 // -P1 -H1 add0r. rewrite -{2}P1. case: (Req_EM_T (P a) 0) => Hi. - rewrite Hi mulR0 !add0R. + rewrite Hi mulr0 !add0r. + rewrite gtr_pMl//. rewrite Hi add0r in P1. - by rewrite P1 mulR1 add0r. + by rewrite P1. case: (Req_EM_T (P b) 0) => Hj. rewrite Hj addr0 in P1. - rewrite Hj mulR0 !addR0 P1 mulR1. - rewrite addr0. - by rewrite ltR_subl_addr ltR_addl. - case/Rle_lt_or_eq_dec : H1 => H1. - - apply leR_lt_add. - + rewrite -{2}(mul1R (P a)); apply leR_wpmul2r => //. - by rewrite leR_subl_addr leR_addl; exact: ltRW. - + rewrite -{2}(mul1R (P b)); apply ltR_pmul2r => //. - by apply/RltP; rewrite lt0r; apply/andP; split; [exact/eqP|by []]. - - rewrite -H1 mulR0 add0R add0r. + rewrite Hj mulr0 !addr0 P1 mulr1. + by rewrite ltrBlDr ltrDl. + move: H1; rewrite le_eqVlt => /predU1P[|] H1; last first. + - apply ler_ltD. + + rewrite -{2}(mul1r (P a)); apply ler_wpM2r => //. + by rewrite lerBlDr ler_addl; exact: ltW. + + rewrite -{2}(mul1r (P b)) ltr_pM2r //. + by rewrite lt0r; apply/andP; split; [exact/eqP|by []]. + - rewrite -H1 mulr0 add0r add0r. have -> : P b = 1 by rewrite -P1 -H1 add0r. - by rewrite mulR1. -rewrite (_ : forall a b, - (a + b) = - a - b); last by move=> *; field. -rewrite -mulNR. + by rewrite mulr1. +rewrite (_ : forall a b, - (a + b) = - a - b); last by move=> *; lra. +rewrite -mulNr. set q := (1 - p) * P a + p * P b. -apply: (@leR_trans (H2 q)); last exact: H2_max. +have H01' : 0 <= (1 - p) * P a + p * P b <= 1. + by case/andP : H01 => /ltW -> /ltW ->. +apply: (@le_trans _ _ (H2 q)); last first. + rewrite (entropy_H2 card_A (@Prob.mk _ q H01'))//. + rewrite (le_trans (entropy_max _))// card_A. + + +exact: H2_max. by rewrite /H2 !mulNR; apply Req_le; field. Qed. diff --git a/information_theory/shannon_fano.v b/information_theory/shannon_fano.v index 21495e93..008c88d9 100644 --- a/information_theory/shannon_fano.v +++ b/information_theory/shannon_fano.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 ssralg ssrnum. -Require Import Reals. -From mathcomp Require Import Rstruct. -Require Import ssrZ ssrR logb Reals_ext realType_ext ssr_ext fdist. +From mathcomp Require Import all_ssreflect all_algebra archimedean. +From mathcomp Require Import Rstruct reals. +Require Import ssrZ ssr_ext realType_logb realType_ext fdist bigop_ext. Require Import entropy kraft. (******************************************************************************) @@ -19,13 +18,13 @@ Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. -Local Open Scope R_scope. +Local Open Scope ring_scope. -Import Order.POrderTheory Num.Theory. +Import Order.POrderTheory Num.Theory GRing.Theory. Definition kraft_condR (T : finType) (sizes : seq nat) := let n := size sizes in - (\sum_(i < n) #|T|%:R^-(nth O sizes i) <= (1 : R))%R. + (\sum_(i < n) #|T|%:R^-(nth O sizes i) <= (1 : Rdefinitions.R))%R. Local Open Scope fdist_scope. @@ -44,7 +43,7 @@ Variables (A T : finType) (P : {fdist A}). Local Open Scope zarith_ext_scope. Definition is_shannon_fano (f : Encoding.t A T) := - forall s, size (f s) = '| ceil (Log #|T|%:R (1 / P s)%R) |. + forall s, size (f s) = `| Num.ceil (Log #|T|%:R (P s)^-1%R) |%N. End shannon_fano_def. @@ -65,30 +64,22 @@ Lemma shannon_fano_is_kraft : is_shannon_fano P f -> kraft_condR T sizes. Proof. move=> H. rewrite /kraft_condR. -rewrite (_ : 1 = 1%mcR)//. rewrite -(FDist.f1 P) /sizes size_map. rewrite (eq_bigr (fun i:'I_(size(enum A)) => #|'I_t|%:R ^- size (f (nth a (enum A) i)))); last first. - move=> i _; by rewrite /= (nth_map a). + by move=> i _; rewrite /= (nth_map a)// FDist.f1. rewrite -(big_mkord xpredT (fun i => #|T|%:R ^- size (f (nth a (enum A) i)))). rewrite -(big_nth a xpredT (fun i => #|'I_t|%:R ^- size (f i))). rewrite enumT. -apply leR_sumR => i _. +apply ler_sum => i _. rewrite H. -have Pi0 : 0 < P i by apply/RltP; rewrite lt0r Pr0/=. -apply (@leR_trans (Exp #|T|%:R (- Log #|T|%:R (1 / P i)))); last first. - rewrite div1R LogV// oppRK LogK //; first by apply/RleP; rewrite lexx. - by rewrite (_ : 1 = 1%:R) // ltR_nat card_ord. -rewrite pow_Exp; last by apply ltR0n; rewrite card_ord. -rewrite Exp_Ropp. -apply/leR_inv/Exp_le_increasing => //. - by rewrite (_ : 1 = 1%:R) // ltR_nat card_ord. -rewrite INR_Zabs_nat; last first. - case/boolP : (P i == 1) => [/eqP ->|Pj1]. - by rewrite divR1 Log_1 /ceil fp_R0 eqxx /=; apply/Int_part_ge0. - apply/leR0ceil/ltRW/ltR0Log. - by rewrite (_ : 1 = 1%:R) // ltR_nat card_ord. - rewrite div1R invR_gt1 // ltR_neqAle; split => //; exact/eqP. -by set x := Log _ _; case: (ceilP x). +have Pi0 : 0 < P i by rewrite lt0r Pr0/=. +apply (@le_trans _ _ (Exp #|T|%:R (- Log #|T|%:R (P i)^-1))); last first. + by rewrite LogV// opprK LogK // card_ord natn. +rewrite pow_Exp; last by rewrite card_ord. +rewrite Exp_oppr lef_pV2// ?posrE ?Exp_gt0//. +rewrite !card_ord natn Exp_le_increasing//. +rewrite (le_trans (mathcomp_extra.ceil_ge _))//. +by rewrite natr_absz// ler_int ler_norm. Qed. End shannon_fano_is_kraft. @@ -116,28 +107,29 @@ Lemma shannon_fano_average_entropy : is_shannon_fano P f -> average P f < `H P + 1. Proof. move=> H; rewrite /average. -apply (@ltR_leR_trans (\sum_(x in A) P x * (- Log #|T|%:R (P x) + 1))). +apply (@lt_le_trans _ _ (\sum_(x in A) P x * (- Log #|T|%:R (P x) + 1))). apply: ltR_sumR. apply: fdist_card_neq0. exact: P. move=> i. - apply ltR_pmul2l; first by apply/RltP; rewrite lt0r Pr_pos /=. + rewrite ltr_pM2l//; last by apply/fdist_gt0. rewrite H. rewrite (_ : #|T|%:R = 2) // ?card_ord // -!/(log _). - set x := log _; case: (ceilP x) => _ Hx. - have Pi0 : 0 < P i by apply/RltP; rewrite lt0r Pr_pos /=. - rewrite INR_Zabs_nat; last first. - apply/leR0ceil. - rewrite /x div1R /log LogV //. - apply oppR_ge0. - by rewrite -(Log_1 2); apply Log_increasing_le. - case: (ceilP x) => _. - by rewrite -LogV // -/(log _) -(div1R _) /x. -under eq_bigr do rewrite mulRDr mulR1 mulRN. -rewrite big_split /= FDist.f1 leR_add2r. -apply Req_le. -rewrite /entropy big_morph_oppR; apply eq_bigr => i _. -by rewrite card_ord (_ : 2%:R = 2). + set x := log _. + rewrite -ltrBlDr. + rewrite (le_lt_trans _ (gt_pred_ceil _))// ?num_real//. + rewrite natr_absz. + rewrite intrD lerB// ler_int. + rewrite /x logV -?fdist_gt0//. + rewrite -[leRHS]gez0_abs//. + rewrite -mathcomp_extra.ceil_ge0//. + rewrite (@lt_le_trans _ _ 0)// ?ltrN10// lerNr oppr0. + by rewrite -log1 ler_log// ?posrE// -fdist_gt0. +under eq_bigr do rewrite mulrDr mulr1 mulrN. +rewrite big_split /= FDist.f1 lerD2r. +rewrite le_eqVlt; apply/orP; left; apply/eqP. +rewrite /entropy big_morph_oppr; apply eq_bigr => i _. +by rewrite card_ord /log//. Qed. End shannon_fano_suboptimal. diff --git a/lib/binary_entropy_function.v b/lib/binary_entropy_function.v index 17430093..4e40f265 100644 --- a/lib/binary_entropy_function.v +++ b/lib/binary_entropy_function.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 ssralg ssrnum. -From mathcomp Require Import reals. -Require Import Reals Lra. -Require Import ssrR Reals_ext Ranalysis_ext realType_logb. +From mathcomp Require Import all_ssreflect all_algebra. +From mathcomp Require Import Rstruct reals exp lra. +Require Import ssr_ext realType_ext realType_logb. (******************************************************************************) (* The natural entropy function *) @@ -22,11 +21,13 @@ Set Implicit Arguments. Unset Strict Implicit. Import Prenex Implicits. -Local Open Scope R_scope. +Local Open Scope ring_scope. + +Import Order.POrderTheory GRing.Theory Num.Theory. Definition H2ln {R : realType} : R -> R := fun p : R => (- p * exp.ln p - (1 - p) * exp.ln (1 - p))%mcR. -Lemma derivable_pt_ln_Rminus x : x < 1 -> derivable_pt ln (1 - x). +(*Lemma derivable_pt_ln_Rminus x : x < 1 -> derivable_pt ln (1 - x). Proof. move=> Hx. exists (/ (1 - x)). @@ -34,7 +35,6 @@ apply derivable_pt_lim_ln, subR_gt0. assumption. Defined. -(* Lemma pderivable_H2ln : pderivable H2ln (fun x => 0 < x <= 1/2). Proof. move=> x /= [Hx0 Hx1]. @@ -140,17 +140,22 @@ rewrite /H2 /log. by rewrite !(Log_1, mulR0, mul0R, oppR0, mul1R, mulR1, add0R, addR0, subR0, subRR). Qed. +*) -Lemma H2_max : forall p, 0 < p < 1 -> H2 p <= 1. +(* +Lemma H2_max : forall p : Rdefinitions.R, 0 < p < 1 -> H2 p <= 1. Proof. -move=> p [Hp0 Hp1]. +move=> p /andP[Hp0 Hp1]. rewrite /H2. -apply (@leR_pmul2l (ln 2)) => //. -rewrite mulR1 mulRDr /log -!mulNR !(mulRC (ln 2)) -!mulRA. -rewrite (mulVR _ ln2_neq0) !mulR1 (mulNR (1 - p)); exact/H2ln_max. +rewrite -(@ler_pM2l _ (ln 2))// ?ln2_gt0//. +rewrite mulr1 mulrDr /log -!mulNr !(mulrC (ln 2)) -!mulrA. +rewrite (@mulVf _ _ ln2_neq0) !mulr1 (mulNr (1 - p)). + +; exact/H2ln_max. Qed. +*) -Lemma H2_max' (x : R): 0 <= x <= 1 -> H2 x <= 1. +(*Lemma H2_max' (x : R): 0 <= x <= 1 -> H2 x <= 1. Proof. move=> [x_0 x_1]. case: x_0 => [?|<-]; last by rewrite bin_ent_0eq0. diff --git a/lib/logb.v b/lib/logb.v index c04cd978..88c73537 100644 --- a/lib/logb.v +++ b/lib/logb.v @@ -414,4 +414,3 @@ rewrite big_cons LogM//; last first. by apply/RltP/prodr_gt0 => a _; exact/RltP. by rewrite [RHS]big_cons oppRD; congr (_ + _)%coqR. Qed. - diff --git a/lib/realType_ext.v b/lib/realType_ext.v index 01f875e4..fafb3a39 100644 --- a/lib/realType_ext.v +++ b/lib/realType_ext.v @@ -609,3 +609,71 @@ rewrite subr_eq0. apply: contra H1 => /eqP H1. by apply/eqP/val_inj; rewrite /= p_of_rsE. Qed. + +Section leR_ltR_sumR_finType. +Context {R : realType}. +Variables (A : finType) (f g : A -> R) (P Q : pred A). +Local Open Scope ring_scope. + +Lemma leR_sumR_support (X : {set A}) : + (forall i, i \in X -> P i -> f i <= g i) -> + \sum_(i in X | P i) f i <= \sum_(i in X | P i) g i. +Proof. +move=> H; elim/big_rec2 : _ => //. +move=> a x y /andP[aX Pa] yx. +by apply lerD => //; apply: H. +Qed. + +Lemma leR_sumRl : (forall i, P i -> f i <= g i) -> + (forall i, Q i -> 0 <= g i) -> (forall i, P i -> Q i) -> + \sum_(i | P i) f i <= \sum_(i | Q i) g i. +Proof. +move=> f_g Qg H; elim: (index_enum _) => [| h t IH]. +- rewrite !big_nil. + by rewrite lexx. +- rewrite !big_cons /=; case: ifP => [Ph|Ph]. + by rewrite (H _ Ph); apply lerD => //; exact: f_g. + case: ifP => // Qh; apply: (le_trans IH). + by rewrite -{1}[X in X <= _](add0r _) lerD2r Qg. +Qed. + +Lemma leR_sumRl_support (U : pred A) : + (forall a, 0 <= f a) -> (forall i, P i -> Q i) -> + \sum_(i in U | P i) f i <= \sum_(i in U | Q i) f i. +Proof. +move=> Hf P_Q; elim: (index_enum _) => [|h t IH]. +- by rewrite !big_nil lexx. +- rewrite !big_cons; case: (h \in U) => //=; case: ifP => // Ph. + + by case: ifP => [Qh|]; [rewrite lerD2l | rewrite (P_Q _ Ph)]. + + by case: ifP => // Qh; rewrite -[X in X <= _]add0r; exact/lerD. +Qed. + +Lemma ltR_sumR_support (X : {set A}) : (0 < #|X|)%nat -> + (forall i, i \in X -> f i < g i) -> + \sum_(i in X) f i < \sum_(i in X) g i. +Proof. +move Hn : #|X| => n; elim: n X Hn => // n IH X Hn _ H. +move: (ltn0Sn n); rewrite -Hn card_gt0; case/set0Pn => a0 Ha0. +rewrite (@big_setD1 _ _ _ _ a0 _ f) //= (@big_setD1 _ _ _ _ a0 _ g) //=. +case: n => [|n] in IH Hn. + rewrite (_ : X :\ a0 = set0); first by rewrite !big_set0 2!addr0; exact: H. + move: Hn. + by rewrite (cardsD1 a0) Ha0 /= add1n => -[] /eqP; rewrite cards_eq0 => /eqP. +apply ltrD; first exact/H. +apply IH => //. +- by move: Hn; rewrite (cardsD1 a0) Ha0 /= add1n => -[]. +- by move=> a; rewrite in_setD inE => /andP[_ ?]; exact: H. +Qed. + +Lemma ltR_sumR : (O < #|A|)%nat -> (forall i, f i < g i) -> + \sum_(i in A) f i < \sum_(i in A) g i. +Proof. +move=> A0 H0. +have : forall i : A, i \in [set: A] -> f i < g i by move=> a _; exact/H0. +move/ltR_sumR_support; rewrite cardsT => /(_ A0). +rewrite big_mkcond /= [in X in _ < X]big_mkcond /=. +rewrite (eq_bigr f) //; last by move=> *; rewrite inE. +by rewrite [in X in _ < X](eq_bigr g) // => *; rewrite inE. +Qed. + +End leR_ltR_sumR_finType. diff --git a/lib/realType_logb.v b/lib/realType_logb.v index b2fd1eac..957d583a 100644 --- a/lib/realType_logb.v +++ b/lib/realType_logb.v @@ -112,6 +112,42 @@ Proof. by move=> x0 y0; rewrite LogM ?invr_gt0// LogV. Qed. End Log. +Section Exp. +Context {R : realType}. + +Definition Exp (n : nat) (x : R) := expR (x * ln n%:R). + +Lemma pow_Exp (x : nat) n : (0 < x)%N -> x%:R ^+ n = Exp x n%:R. +Proof. by move=> x0; rewrite /Exp expRM_natl lnK// posrE ltr0n. Qed. + +Lemma LogK n x : (1 < n)%N -> 0 < x -> Exp n (Log n x) = x. +Proof. +move=> n1 x0. +rewrite /Log /Exp prednK// 1?ltnW// -mulrA mulVf// ?mulr1 ?lnK//. +by rewrite gt_eqF// -ln1 ltr_ln// ?posrE// ?ltr1n// ltr0n ltnW. +Qed. + +Lemma Exp_oppr n x : Exp n (- x) = (Exp n x)^-1. +Proof. by rewrite /Exp mulNr expRN. Qed. + +Lemma Exp_gt0 n x : 0 < Exp n x. Proof. by rewrite /Exp expR_gt0. Qed. + +Lemma Exp_ge0 n x : 0 <= Exp n x. Proof. exact/ltW/Exp_gt0. Qed. + +Lemma Exp_increasing n x y : (1 < n)%N -> x < y -> Exp n x < Exp n y. +Proof. by move=> ? ?; rewrite ltr_expR// ltr_pM2r// ln_gt0// ltr1n. Qed. + +Lemma Exp_le_increasing n x y : (1 < n)%N -> x <= y -> Exp n x <= Exp n y. +Proof. +move=> n1; rewrite /Exp le_eqVlt => /predU1P[->//|]. +by move/Exp_increasing => x_y; exact/ltW/x_y. +Qed. + +End Exp. + +Hint Extern 0 (0 < Exp _ _) => solve [exact/Exp_gt0] : core. + +Hint Extern 0 (0 <= Exp _ _) => solve [exact/Exp_ge0] : core. Section log. Context {R : realType}. @@ -121,6 +157,8 @@ Definition log {R : realType} (x : R) := Log 2 x. Lemma log1 : log 1 = 0 :> R. Proof. by rewrite /log Log1. Qed. +Lemma log2 : log 2 = 1 :> R. Proof. by rewrite /log /Log prednK// divff// gt_eqF// ln2_gt0. Qed. + Lemma ler_log : {in Num.pos &, {mono log : x y / x <= y :> R}}. Proof. by move=> x y x0 y0; rewrite /log ler_Log. Qed. @@ -151,3 +189,16 @@ exact/ln_id_cmp. Qed. End log. + +Lemma log_prodr_sumr_mlog {R : realType} {A : finType} (f : A -> R) s : + (forall a, 0 <= f a) -> + (forall i, 0 < f i) -> + (- log (\prod_(i <- s) f i) = \sum_(i <- s) - log (f i))%R. +Proof. +move=> f0 f0'. +elim: s => [|h t ih]. + by rewrite !big_nil log1 oppr0. +rewrite big_cons logM//; last first. + by apply/prodr_gt0 => a _. +by rewrite [RHS]big_cons opprD ih. +Qed.