contents of proba.v moved to fdist.v,

renamed cproba.v to jfdist.v,
minor doc additions

renamings:
- CFDist -> CJFDist
- CondFDist -> CondJFDist0
- CondFDistT -> CondJFDist
notations:
- P `(| a ) for CondFDistT.d

_CoqProject

@@ -20,12 +20,13 @@ lib/euclid.v
 lib/dft.v
 lib/vandermonde.v
 lib/classical_sets_ext.v
+probability/fdist.v
 probability/proba.v
 probability/convex_type.v
 probability/convex_choice.v
 probability/fsdist.v
 probability/convex_stone.v
-probability/cproba.v
+probability/jfdist.v
 probability/cinde.v
 probability/jensen.v
 probability/ln_facts.v

changelog.txt

@@ -6,6 +6,14 @@ renamings:
 - setX1' -> setX1r (direction change)
 - setX0 -> setX0r
 - Int_part_pos -> Int_part_ge0
+- CFDist -> CJFDist
+- CondFDist -> CondJFDist0
+- CondFDistT -> CondJFDist
 
-files
+notations:
+- P `(| a ) for CondFDistT.d
+
+files:
 - pinsker_fun.v has been integrated into pinsker.v
+- proba.v renamed to fdist.v (proba.v kept for compatibility)
+- cproba.v renamed to jfdist.v

ecc_classic/decoding.v

@@ -2,7 +2,7 @@
 From mathcomp Require Import all_ssreflect ssralg fingroup finalg perm zmodp.
 From mathcomp Require Import matrix vector.
 Require Import Reals Lra.
-Require Import ssrR Reals_ext ssr_ext ssralg_ext Rbigop f2 proba.
+Require Import ssrR Reals_ext ssr_ext ssralg_ext Rbigop f2 fdist.
 Require Import channel_code channel binary_symmetric_channel hamming pproba.
 
 (******************************************************************************)

ecc_classic/hamming_code.v

@@ -2,7 +2,7 @@
 From mathcomp Require Import all_ssreflect ssralg fingroup finalg perm zmodp.
 From mathcomp Require Import matrix mxalgebra vector.
 Require Import ssr_ext ssralg_ext f2 linearcode natbin ssrR hamming bigop_ext.
-Require Import Rbigop proba channel channel_code decoding.
+Require Import Rbigop fdist channel channel_code decoding.
 Require Import binary_symmetric_channel.
 
 (******************************************************************************)

ecc_modern/checksum.v

@@ -2,7 +2,7 @@
 From mathcomp Require Import all_ssreflect ssralg fingroup finalg perm zmodp.
 From mathcomp Require Import matrix vector.
 Require Import Reals.
-Require Import ssralg_ext ssrR Reals_ext f2 proba channel tanner linearcode.
+Require Import ssralg_ext ssrR Reals_ext f2 fdist channel tanner linearcode.
 Require Import Rbigop pproba.
 
 Set Implicit Arguments.

ecc_modern/degree_profile.v

@@ -1,7 +1,7 @@
 From mathcomp Require Import all_ssreflect ssralg fingroup zmodp poly ssrnum.
 From mathcomp Require Import matrix perm.
 From mathcomp Require boolp.
-Require Import ssr_ext ssralg_ext ssrR proba.
+Require Import ssr_ext ssralg_ext ssrR fdist.
 
 (******************************************************************************)
 (*                  Work in progress about LDPC codes                         *)

ecc_modern/ldpc.v

@@ -3,7 +3,7 @@ From mathcomp Require Import all_ssreflect ssralg fingroup finalg perm zmodp.
 From mathcomp Require Import matrix vector.
 Require Import Reals Lra.
 Require Import ssrR Reals_ext ssr_ext ssralg_ext num_occ bigop_ext Rbigop.
-Require Import proba channel pproba f2 linearcode subgraph_partition tanner.
+Require Import fdist channel pproba f2 linearcode subgraph_partition tanner.
 Require Import tanner_partition hamming binary_symmetric_channel decoding.
 Require Import channel_code summary checksum summary_tanner.
 

ecc_modern/ldpc_algo.v

@@ -2,7 +2,7 @@
 Require Import Wf Recdef Reals.
 From mathcomp Require Import all_ssreflect perm zmodp matrix ssralg.
 Require Import ssrR Reals_ext Rbigop f2 subgraph_partition tanner.
-Require Import proba channel pproba linearcode ssralg_ext.
+Require Import fdist channel pproba linearcode ssralg_ext.
 Require Import tanner_partition summary ldpc checksum.
 
 (** * Sum-Product Decoder *)

ecc_modern/ldpc_algo_proof.v

@@ -2,7 +2,7 @@
 Require Import Wf_nat Wf Recdef Reals.
 From mathcomp Require Import all_ssreflect perm zmodp matrix ssralg.
 Require Import ssrR Reals_ext Rbigop f2 subgraph_partition tanner.
-Require Import proba channel pproba linearcode ssralg_ext.
+Require Import fdist channel pproba linearcode ssralg_ext.
 Require Import tanner_partition summary ldpc checksum ldpc_algo.
 
 (** * Verification of the Sum-Product decoder *)

ecc_modern/subgraph_partition.v

@@ -3,9 +3,11 @@ From mathcomp Require Import all_ssreflect ssralg fingroup finalg perm zmodp.
 From mathcomp Require Import matrix.
 Require Import ssr_ext.
 
-(** * Bipartite/acyclic graphs, cover/partition properties *)
+(******************************************************************************)
+(*          Cover/partition properties of bipartite-acyclic graphs            *)
+(******************************************************************************)
 
-(** OUTLINE:
+(* OUTLINE:
 - Section colorable.
 - Section bipartite.
 - Section simple.

ecc_modern/summary.v

@@ -3,9 +3,20 @@ From mathcomp Require Import all_ssreflect ssralg fingroup finalg zmodp matrix.
 Require Import Reals.
 Require Import ssr_ext ssralg_ext ssrR Rbigop f2.
 
-(** * The Summary Operator *)
-
-(** OUTLINE:
+(******************************************************************************)
+(*                        The Summary Operator                                *)
+(*                                                                            *)
+(* This file provides a formalization of the summary operator used in         *)
+(* pencil-and-paper proofs in modern coding theory.                           *)
+(*                                                                            *)
+(* Definitions:                                                               *)
+(*   \sum_( x = d [~ s]) F == summation over the vectors x equal to d on all  *)
+(*                            components except the freely enumerated         *)
+(*                            indices in s                                    *)
+(*   summary_fold r d e    == alternative expression of \sum_( x = d [~ r]) e *)
+(******************************************************************************)
+
+(* OUTLINE:
 - Section free_on.
 - Section rsum_freeon.
 - Section alternative_definitions_of_summary.

ecc_modern/summary_tanner.v

@@ -2,12 +2,14 @@
 From mathcomp Require Import all_ssreflect ssralg fingroup finalg zmodp matrix.
 Require Import Reals.
 Require Import ssr_ext ssralg_ext ssrR Reals_ext Rbigop f2 summary.
-Require Import subgraph_partition tanner tanner_partition proba channel.
+Require Import subgraph_partition tanner tanner_partition fdist channel.
 Require Import checksum.
 
-(** * Technical lemmas about the summary operator *)
+(******************************************************************************)
+(*               Technical lemmas about the summary operator                  *)
+(******************************************************************************)
 
-(** OUTLINE
+(* OUTLINE
 - Section dprojs_comb.
 - Section dproj_F2.
 - Section dprojs_subgraph.

ecc_modern/tanner.v

@@ -3,9 +3,15 @@ From mathcomp Require Import all_ssreflect ssralg fingroup finalg perm zmodp.
 From mathcomp Require Import matrix.
 Require Import bigop_ext ssralg_ext f2 subgraph_partition.
 
-(** * Tanner Graphs *)
-
-(** OUTLINE:
+(******************************************************************************)
+(*                           Tanner Graphs                                    *)
+(*                                                                            *)
+(* 'F(m0, n0) == function nodes of the subgraph rooted at edge m0-n0          *)
+(* ‘V(m0, n0) == the variable nodes of the subgraph rooted at edge m0-n0      *)
+(*               (to which we add n0)                                         *)
+(******************************************************************************)
+
+(* OUTLINE:
 - Module Tanner.
 - Section tanner_relation.
 - Section next_graph.
@@ -176,7 +182,7 @@ apply/andP; split => //.
 by rewrite last_rcons.
 Qed.
 
-Lemma Fgraph_Vnext2_Vgraph m0 n0 m1 n1 : 
+Lemma Fgraph_Vnext2_Vgraph m0 n0 m1 n1 :
   m1 \in 'F(m0, n0) -> n1 \in 'V m1 -> n0 \in 'V m0 -> n1 \in 'V(m0, n0).
 Proof.
 move=> Hm1 Hn1 Hm0.

ecc_modern/tanner_partition.v

@@ -3,18 +3,20 @@ From mathcomp Require Import all_ssreflect ssralg fingroup finalg perm zmodp.
 From mathcomp Require Import matrix.
 Require Import ssr_ext subgraph_partition tanner f2 Rbigop.
 
-Set Implicit Arguments.
-Unset Strict Implicit.
-Import Prenex Implicits.
-
-(** * Cover/partition properties of Tanner graphs *)
+(******************************************************************************)
+(*               Cover/partition properties of Tanner graphs                  *)
+(******************************************************************************)
 
-(** OUTLINE:
+(* OUTLINE:
 - Section tanner_rel_no_hypo.
 - Section acyclic_tanner_rel.
 - Section tanner_partition.
 *)
 
+Set Implicit Arguments.
+Unset Strict Implicit.
+Import Prenex Implicits.
+
 Import GRing.
 Local Open Scope ring_scope.
 

information_theory/aep.v

@@ -3,7 +3,7 @@
 From mathcomp Require Import all_ssreflect ssralg fingroup finalg matrix.
 From mathcomp Require boolp.
 Require Import Reals.
-Require Import ssrR Reals_ext ssr_ext ssralg_ext logb Rbigop proba entropy.
+Require Import ssrR Reals_ext ssr_ext ssralg_ext logb Rbigop fdist entropy.
 
 (******************************************************************************)
 (*              Asymptotic Equipartition Property (AEP)                       *)

information_theory/binary_symmetric_channel.v

@@ -1,9 +1,9 @@
 (* infotheo (c) AIST. R. Affeldt, M. Hagiwara, J. Senizergues. GNU GPLv3. *)
 (* infotheo v2 (c) AIST, Nagoya University. GNU GPLv3. *)
 From mathcomp Require Import all_ssreflect ssralg finset fingroup finalg perm.
-From mathcomp Require Import  zmodp matrix.
+From mathcomp Require Import zmodp matrix.
 Require Import Reals Lra.
-Require Import ssrR Reals_ext logb ssr_ext ssralg_ext bigop_ext Rbigop proba.
+Require Import ssrR Reals_ext logb ssr_ext ssralg_ext bigop_ext Rbigop fdist.
 Require Import entropy binary_entropy_function channel hamming channel_code.
 
 (******************************************************************************)

information_theory/channel.v

@@ -2,12 +2,14 @@
 (* infotheo v2 (c) AIST, Nagoya University. GNU GPLv3. *)
 From mathcomp Require Import all_ssreflect ssralg fingroup finalg matrix.
 Require Import Reals.
-Require Import ssrR Reals_ext logb ssr_ext ssralg_ext bigop_ext Rbigop proba.
-Require Import entropy cproba chap2.
+Require Import ssrR Reals_ext logb ssr_ext ssralg_ext bigop_ext Rbigop fdist.
+Require Import entropy jfdist chap2.
 
-(** * Definition of channels and of the capacity *)
+(******************************************************************************)
+(*                 Definition of channels and of the capacity                 *)
+(******************************************************************************)
 
-(** OUTLINE:
+(* OUTLINE:
   1. Module Channel1.
      Probability transition matrix
   2. Module DMC.
@@ -309,10 +311,10 @@ Let QP := Swap.d (`J(P, W)).
 Lemma channel_cPr : forall a b, P a != 0 -> W a b = \Pr_QP[[set b]|[set a]].
 Proof.
 move=> a b Pa0.
-rewrite (@CFDist.E _ _ (CFDist.mkt P W)) //=; last exact/eqP.
+rewrite (@CJFDist.E _ _ (CJFDist.mkt P W)) //=; last exact/eqP.
 congr cPr.
 apply/fdist_ext => -[b0 a0].
-by rewrite !Swap.dE JointFDistChan.dE /= /CFDist.joint_of /= ProdFDist.dE.
+by rewrite !Swap.dE JointFDistChan.dE /= /CJFDist.joint_of /= ProdFDist.dE.
 Qed.
 
 End relation_channel_cproba.

information_theory/channel_code.v

@@ -1,9 +1,11 @@
 (* infotheo (c) AIST. R. Affeldt, M. Hagiwara, J. Senizergues. GNU GPLv3. *)
 From mathcomp Require Import all_ssreflect ssralg fingroup finalg matrix.
 Require Import Reals.
-Require Import Reals_ext ssrR logb Rbigop proba channel.
+Require Import Reals_ext ssrR logb Rbigop fdist channel.
 
-(** * Definition of a channel code *)
+(******************************************************************************)
+(*                        Definition of a channel code                        *)
+(******************************************************************************)
 
 Reserved Notation "e( W , c )" (at level 50).
 Reserved Notation "echa( W , c )" (at level 50).

information_theory/channel_coding_converse.v

@@ -3,7 +3,7 @@
 From mathcomp Require Import all_ssreflect ssralg fingroup finalg matrix.
 Require Import Reals.
 Require Import ssrR Reals_ext ssr_ext ssralg_ext logb ln_facts Rbigop arg_rmax.
-Require Import num_occ proba entropy types jtypes divergence.
+Require Import num_occ fdist entropy types jtypes divergence.
 Require Import conditional_divergence error_exponent channel_code channel.
 Require Import success_decode_bound.
 

information_theory/channel_coding_direct.v

@@ -3,7 +3,7 @@
 From mathcomp Require Import all_ssreflect ssralg fingroup finalg matrix perm.
 Require Import Reals Lra Classical.
 Require Import ssrZ ssrR Reals_ext logb ssr_ext ssralg_ext bigop_ext Rbigop.
-Require Import proba entropy aep typ_seq joint_typ_seq channel channel_code.
+Require Import fdist entropy aep typ_seq joint_typ_seq channel channel_code.
 
 (******************************************************************************)
 (*                 Channel coding theorem (direct part)                       *)