fixes #32

_CoqProject

@@ -26,7 +26,7 @@ lib/classical_sets_ext.v
 probability/fdist.v
 probability/proba.v
 probability/fsdist.v
-probability/convex_choice.v
+probability/convex.v
 probability/convex_equiv.v
 probability/convex_stone.v
 probability/jfdist.v

changelog.txt

@@ -71,6 +71,7 @@ from 0.2.2 to 0.3
   + derive_increasing_interv_right -> pderive_increasing_closed_open
   + derive_increasing_ad_hoc -> pderive_ad_hoc
   + ltr_subl_addl -> ltR_subl_addl
+  + convex_choice.v -> convex.v
 
 - removed:
   + from ssrR.v:

information_theory/convex_fdist.v

@@ -5,8 +5,8 @@ From mathcomp Require boolp.
 From mathcomp Require Import Rstruct.
 Require Import Reals Ranalysis_ext Lra.
 Require Import ssrR Reals_ext logb ssr_ext ssralg_ext bigop_ext Rbigop fdist.
-Require Import entropy fdist jfdist convex_choice binary_entropy_function.
-Require Import log_sum divergence chap2.
+Require Import entropy fdist jfdist convex binary_entropy_function log_sum.
+Require Import divergence chap2.
 
 (******************************************************************************)
 (*                Section 2.7 of Elements of Information Theory               *)

information_theory/string_entropy.v

@@ -4,10 +4,10 @@ From mathcomp Require Import all_ssreflect ssralg fingroup finalg matrix.
 Require Import Reals.
 From mathcomp Require Import Rstruct.
 Require Import ssrR Reals_ext ssr_ext ssralg_ext logb Rbigop.
-Require Import fdist entropy convex_choice ln_facts jensen num_occ.
+Require Import fdist entropy convex ln_facts jensen num_occ.
 
 (******************************************************************************)
-(*                        String entropy                                      *)
+(*                         String entropy                                     *)
 (*                                                                            *)
 (* For details, see: Reynald Affeldt, Jacques Garrigue, and Takafumi Saikawa. *)
 (* Examples of formal proofs about data compression. International Symposium  *)

lib/logb.v

@@ -132,7 +132,7 @@ Proof. move=> xpos; by apply Rge_le, Rminus_ge, Rle_ge, exp_dev_ge0. Qed.
 End exp_lower_bound.
 
 End addtional_lemmas_about_ln_exp.
-Hint Resolve ln2_gt0 : core.
+Global Hint Resolve ln2_gt0 : core.
 
 Definition Log (n : R) x := ln x / ln n.
 
@@ -259,8 +259,8 @@ Qed.
 
 Lemma Exp_gt0 n x : 0 < Exp n x. Proof. rewrite /Exp; exact: exp_pos. Qed.
 Lemma Exp_ge0 n x : 0 <= Exp n x. Proof. exact/ltRW/Exp_gt0. Qed.
-Hint Resolve Exp_gt0 : core.
-Hint Resolve Exp_ge0 : core.
+Global Hint Resolve Exp_gt0 : core.
+Global Hint Resolve Exp_ge0 : core.
 
 Lemma Exp_0 n : Exp n 0 = 1.
 Proof. by rewrite /Exp mul0R exp_0. Qed.

probability/convex_equiv.v

@@ -5,7 +5,7 @@ From mathcomp Require Import boolp classical_sets.
 Require Import Reals.
 From mathcomp Require Import Rstruct.
 Require Import ssrR Reals_ext Ranalysis_ext ssr_ext ssralg_ext logb Rbigop.
-Require Import fdist jfdist fsdist convex_choice.
+Require Import fdist jfdist fsdist convex.
 
 (******************************************************************************)
 (*                  Equivalence of Convexity Definitions                      *)

probability/convex_stone.v

@@ -5,7 +5,7 @@ From mathcomp Require boolp.
 Require Import Reals Lra.
 From mathcomp Require Import Rstruct.
 Require Import ssrR Reals_ext Ranalysis_ext ssr_ext ssralg_ext logb Rbigop.
-Require Import fdist convex_choice.
+Require Import fdist convex.
 
 (****************************************************************************)
 (* Direct formalization of the Lemma 2 from M. H. Stone. Postulates for the *)

probability/fsdist.v

@@ -6,7 +6,7 @@ From mathcomp Require boolp.
 Require Import Reals.
 From mathcomp Require Import Rstruct.
 Require Import ssrR Reals_ext ssr_ext ssralg_ext bigop_ext Rbigop fdist.
-Require Import convex_choice.
+Require Import convex.
 
 (******************************************************************************)
 (*                    Finitely-supported distributions                        *)

probability/jensen.v

@@ -4,7 +4,7 @@ From mathcomp Require Import all_ssreflect ssralg fingroup finalg matrix.
 From mathcomp Require Import boolp Rstruct.
 Require Import Reals.
 Require Import ssrR Reals_ext ssr_ext ssralg_ext logb Rbigop.
-Require Import fdist proba convex_choice.
+Require Import fdist proba convex.
 
 (******************************************************************************)
 (*                           Jensen's inequality                              *)

probability/ln_facts.v

@@ -4,7 +4,7 @@ From mathcomp Require Import all_ssreflect.
 From mathcomp Require boolp.
 From mathcomp Require Import Rstruct.
 Require Import Reals Lra.
-Require Import ssrR Reals_ext Ranalysis_ext logb convex_choice.
+Require Import ssrR Reals_ext Ranalysis_ext logb convex.
 
 (******************************************************************************)
 (*                      Results about the Analysis of ln                      *)

probability/necset.v

@@ -5,7 +5,7 @@ From mathcomp Require Import all_ssreflect.
 From mathcomp Require Import boolp classical_sets Rstruct.
 From mathcomp Require Import finmap.
 Require Import Reals_ext classical_sets_ext Rbigop ssrR fdist fsdist.
-Require Import convex_choice.
+Require Import convex.
 
 (******************************************************************************)
 (*       Semi-complete semilattice structures and non-empty convex sets       *)