divergence.v done

information_theory/entropy.v

@@ -4,7 +4,7 @@ From mathcomp Require Import all_ssreflect all_algebra fingroup perm.
 Require Import Reals.
 From mathcomp Require Import Rstruct reals.
 Require Import ssrR Reals_ext realType_ext ssr_ext ssralg_ext bigop_ext.
-Require Import logb ln_facts fdist jfdist_cond proba binary_entropy_function.
+Require Import realType_logb (*ln_facts*) fdist jfdist_cond proba binary_entropy_function.
 Require Import divergence.
 
 (******************************************************************************)
@@ -61,10 +61,14 @@ Local Open Scope vec_ext_scope.
 
 Import Order.POrderTheory GRing.Theory Num.Theory.
 
+(* TODO: kludge *)
+Hint Extern 0 ((0 <= _)%coqR) => solve [exact/RleP/FDist.ge0] : core.
+Hint Extern 0 ((_ <= 1)%coqR) => solve [exact/RleP/FDist.le1] : core.
+
 Section entropy_definition.
 Variables (A : finType) (P : {fdist A}).
 
-Definition entropy := - \sum_(a in A) P a * log (P a).
+Definition entropy := - \sum_(a in A) P a * realType_logb.log (P a).
 Local Notation "'`H'" := (entropy).
 
 Lemma entropy_ge0 : 0 <= `H.
@@ -73,8 +77,8 @@ rewrite /entropy big_morph_oppR; apply/RleP/sumr_ge0 => i _; apply/RleP.
 have [->|Hi] := eqVneq (P i) 0; first by rewrite mul0R oppR0.
   (* NB: this step in a standard textbook would be handled as a consequence of lim x->0 x log x = 0 *)
 rewrite mulRC -mulNR; apply mulR_ge0 => //; apply: oppR_ge0.
-rewrite -log1; apply: Log_increasing_le => //.
-by apply/RltP; rewrite lt0r Hi/=.
+rewrite coqRE -(@log1 R); apply/RleP; rewrite ler_log// ?posrE//.
+by rewrite lt0r Hi/=.
 Qed.
 
 End entropy_definition.
@@ -93,13 +97,14 @@ rewrite /entropy /log_RV /= big_morph_oppR.
 by apply eq_bigr => a _; rewrite mulRC -mulNR.
 Qed.
 
-Lemma xlnx_entropy (P : {fdist A}) : `H P = / ln 2 * - \sum_(a : A) xlnx (P a).
+Lemma xlnx_entropy (P : {fdist A}) : `H P = / exp.ln 2 * - \sum_(a : A) xlnx (P a).
 Proof.
 rewrite /entropy mulRN; congr (- _); rewrite big_distrr/=.
-apply: eq_bigr => a _; rewrite /log /Rdiv mulRA mulRC; congr (_ * _).
-rewrite /xlnx; case : ifP => // /RltP Hcase.
-have -> : P a = 0 by case (Rle_lt_or_eq_dec 0 (P a)).
-by rewrite mul0R.
+apply: eq_bigr => a _; rewrite /xlnx /log /Log/=.
+have := FDist.ge0 P a.
+rewrite le_eqVlt => /predU1P[<-|Pa0].
+  by rewrite mul0r if_same mulR0 mul0R.
+by rewrite Pa0 mulRA mulRC !coqRE.
 Qed.
 
 Lemma entropy_uniform n (An1 : #|A| = n.+1) :
@@ -109,8 +114,7 @@ rewrite /entropy.
 under eq_bigr do rewrite fdist_uniformE.
 rewrite big_const iter_addR mulRA RmultE -RinvE.
 rewrite INRE mulRV; last by rewrite An1 -INRE INR_eq0'.
-rewrite -RmultE mul1R logV ?oppRK//; rewrite An1.
-by rewrite -INRE; apply/ltR0n.
+by rewrite -RmultE mul1R !coqRE logV ?An1 ?ltr0n// opprK.
 Qed.
 
 Lemma entropy_H2 (card_A : #|A| = 2%nat) (p : {prob R}) :

lib/binary_entropy_function.v

@@ -1,8 +1,9 @@
 (* 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.
+From mathcomp Require Import all_ssreflect ssralg ssrnum.
+From mathcomp Require Import reals.
 Require Import Reals Lra.
-Require Import ssrR Reals_ext Ranalysis_ext logb.
+Require Import ssrR Reals_ext Ranalysis_ext realType_logb.
 
 (******************************************************************************)
 (*                    The natural entropy function                            *)
@@ -23,7 +24,7 @@ Import Prenex Implicits.
 
 Local Open Scope R_scope.
 
-Definition H2ln := fun p => - p * ln p - (1 - p) * ln (1 - p).
+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).
 Proof.
@@ -33,6 +34,7 @@ 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].
@@ -122,10 +124,11 @@ case: (Rlt_le_dec q (1/2)) => [H1|].
     lra.
   by apply decreasing_on_half_to_1 => //; lra.
 Qed.
+*)
 
-Definition H2 p := - (p * log p) + - ((1 - p) * log (1 - p)).
+Definition H2 {R : realType} (p : R) : R := (- (p * log p) + - ((1 - p) * log (1 - p)))%mcR.
 
-Lemma bin_ent_0eq0 : H2 0 = 0.
+(*Lemma bin_ent_0eq0 : H2 0 = 0.
 Proof.
 rewrite /H2 /log.
 by rewrite !(Log_1, mulR0, mul0R, oppR0, mul1R, mulR1, add0R, addR0, subR0).
@@ -154,3 +157,4 @@ case: x_0 => [?|<-]; last by rewrite bin_ent_0eq0.
 case: x_1 => [?|->]; last by rewrite bin_ent_1eq0.
 exact: H2_max.
 Qed.
+*)

lib/realType_logb.v

@@ -1,7 +1,7 @@
 (* 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 exp.
+From mathcomp Require Import reals exp sequences.
 Require Import realType_ext.
 
 (******************************************************************************)
@@ -21,6 +21,100 @@ Local Open Scope ring_scope.
 
 Import Order.POrderTheory GRing.Theory Num.Theory.
 
-Definition Log {R : realType} (n : R) x := ln x / ln n.
+Section ln_ext.
+Context {R : realType}.
+Implicit Type x : R.
+
+Lemma ln2_gt0 : 0 < ln 2 :> R.
+Proof. by rewrite ln_gt0// ltr1n. Qed.
+
+Lemma ln2_neq0 : ln 2 != 0 :> R. Proof. by rewrite gt_eqF// ln2_gt0. Qed.
+
+Lemma ln_id_cmp x : 0 < x -> ln x <= x - 1.
+Proof.
+move=> x0.
+Admitted.
+
+Lemma ln_id_eq x : 0 < x -> ln x = x - 1 -> x = 1 :> R.
+Proof.
+Admitted.
+
+End ln_ext.
+
+Section xlnx.
+Context {R : realType}.
+
+Definition xlnx (x : R) : R := if (0 < x)%mcR then x * ln x else 0.
+
+Lemma xlnx_0 : xlnx 0 = 0.
+Proof. by rewrite /xlnx mul0r ltxx. Qed.
+
+Lemma xlnx_1 : xlnx 1 = 0.
+Proof. by rewrite /xlnx ltr01 mul1r ln1. Qed.
+
+End xlnx.
+
+
+Section Log.
+Context {R : realType}.
+
+Definition Log (n : nat) x : R := ln x / ln n.-1.+1%:R.
+
+Lemma Log1 (n : nat) : Log n 1 = 0 :> R.
+Proof. by rewrite /Log ln1 mul0r. Qed.
+
+Lemma ler_Log (n : nat) : (1 < n)%N  -> {in Num.pos &, {mono Log n : x y / x <= y :> R}}.
+Proof.
+move=> n1 x y x0 y0.
+rewrite /Log ler_pdivrMr prednK ?(leq_trans _ n1)// ?ln_gt0 ?ltr1n//.
+by rewrite -mulrA mulVf ?mulr1 ?gt_eqF ?ln_gt0 ?ltr1n// ler_ln.
+Qed.
+
+Lemma LogV n x : 0 < x -> Log n x^-1 = - Log n x.
+Proof. by move=> x0; rewrite /Log lnV ?posrE// mulNr. Qed.
+
+Lemma LogM n x y : 0 < x -> 0 < y -> Log n (x * y) = Log n x + Log n y.
+Proof. by move=> *; rewrite /Log -mulrDl lnM. Qed.
+
+Lemma LogDiv n x y : 0 < x -> 0 < y -> Log n (x / y) = Log n x - Log n y.
+Proof. by move=> x0 y0; rewrite LogM ?invr_gt0// LogV. Qed.
+
+End Log.
+
+
+Section log.
+Context {R : realType}.
+Implicit Types x y : R.
 
 Definition log {R : realType} (x : R) := Log 2 x.
+
+Lemma log1 : log 1 = 0 :> R. Proof. by rewrite /log Log1. 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.
+
+Lemma logV x : 0 < x -> log x^-1 = - log x :> R.
+Proof. by move=> x0; rewrite /log LogV. Qed.
+
+Lemma logDiv x y : 0 < x -> 0 < y -> log (x / y) = log x - log y.
+Proof. by move=> x0 y0; exact: (@LogDiv _ _ _ _ x0 y0). Qed.
+
+(* TODO: rename, lemma for Log *)
+Lemma logexp1E : log (expR 1) = (ln 2)^-1 :> R.
+Proof. by rewrite /log /Log/= expRK div1r. Qed.
+
+Lemma log_exp1_Rle_0 : 0 <= log (expR 1) :> R.
+Proof.
+rewrite logexp1E.
+rewrite invr_ge0// ltW//.
+by rewrite ln2_gt0//.
+Qed.
+
+Lemma log_id_cmp x : 0 < x -> log x <= (x - 1) * log (expR 1).
+Proof.
+move=> x0; rewrite logexp1E ler_wpM2r// ?invr_ge0//= ?(ltW (@ln2_gt0 _))//.
+exact/ln_id_cmp.
+Qed.
+
+
+End log.