move the example of computation of conditional entropy to toy_examples,

renaming: dist (over finType) -> fdist, among other changes: {dist _} ->
{fdist _}

_CoqProject

@@ -86,4 +86,7 @@ ecc_modern/max_subset.v
 ecc_modern/stopping_set.v
 ecc_modern/degree_profile.v
 toy_examples/expected_value_variance.v
+toy_examples/expected_value_variance_ordn.v
+toy_examples/expected_value_variance_tuple.v
+toy_examples/conditional_entropy.v
 -R . infotheo

ecc_classic/decoding.v

@@ -102,7 +102,7 @@ Section maximum_likelihood_decoding.
 Variables (A : finFieldType) (B : finType) (W : `Ch(A, B)).
 Variables (n : nat) (C : {vspace 'rV[A]_n}).
 Variable f : decT B [finType of 'rV[A]_n] n.
-Variable P : {dist 'rV[A]_n}.
+Variable P : {fdist 'rV[A]_n}.
 
 Local Open Scope R_scope.
 
@@ -254,7 +254,7 @@ Variable M : finType.
 Variable discard : discardT [finType of 'F_2] n M.
 Variable enc : encT [finType of 'F_2] M n.
 Hypothesis compatible : cancel_on C enc discard.
-Variable P : {dist 'rV['F_2]_n}.
+Variable P : {fdist 'rV['F_2]_n}.
 
 Lemma MD_implies_ML : p < 1/2 -> MD_decoding [set cw in C] f ->
   (forall y, f y != None) -> ML_decoding W C f P.
@@ -308,7 +308,7 @@ Section MAP_decoding.
 Variables (A : finFieldType) (B : finType) (W : `Ch(A, B)).
 Variables (n : nat) (C : {vspace 'rV[A]_n}).
 Variable dec : decT B [finType of 'rV[A]_n] n.
-Variable P : {dist 'rV[A]_n}.
+Variable P : {fdist 'rV[A]_n}.
 
 Definition MAP_decoding := forall y : P.-receivable W,
   exists m, dec y = Some m /\

ecc_modern/degree_profile.v

@@ -450,7 +450,7 @@ Definition fintree_finMixin n l := Eval hnf in FinMixin (@fintree_enumP n l).
 
 Canonical fintree_finType n l := Eval hnf in FinType _ (fintree_finMixin n l).
 
-Definition ensemble n l := {dist (@fintree n l)}.
+Definition ensemble n l := {fdist (@fintree n l)}.
 
 (* maximum branching degree of the graph (root has no parent) *)
 Variable tw : nat.
@@ -706,7 +706,7 @@ evar (h : fintree_finType tw l -> R); rewrite (eq_bigr h); last first.
 by rewrite {}/h -(@big_morph _ _ RofK 0%R Rplus 0%:R (@GRing.add K)) // f1 RofK1.
 Qed.
 
-Definition tree_ensemble l : ensemble tw l := makeDist (@f0R l) (@f1R l).
+Definition tree_ensemble l : ensemble tw l := makeFDist (@f0R l) (@f1R l).
 
 End definition.
 

ecc_modern/ldpc.v

@@ -78,7 +78,7 @@ Hypothesis card_A : #|A| = 2%nat.
 Variable p : R.
 Hypothesis p_01' : 0 < p < 1.
 Let p_01 := Prob.mk (closed p_01').
-Let P : dist A := Uniform.d card_A.
+Let P : fdist A := Uniform.d card_A.
 Variable a' : A.
 Hypothesis Ha' : Receivable.def (P `^ 1) (BSC.c card_A p_01) (\row_(i < 1) a').
 
@@ -87,9 +87,9 @@ Lemma bsc_post (a : A) :
   (if a == a' then 1 - p else p)%R.
 Proof.
 rewrite PosteriorProbability.dE /= /PosteriorProbability.den /=.
-rewrite !TupleDist.dE DMCE big_ord_recl big_ord0.
+rewrite !TupleFDist.dE DMCE big_ord_recl big_ord0.
 rewrite (eq_bigr (fun x : 'M_1 => P a * (BSC.c card_A p_01) ``( (\row__ a') | x))%R); last first.
-  by move=> i _; rewrite /P !TupleDist.dE big_ord_recl big_ord0 !Uniform.dE mulR1.
+  by move=> i _; rewrite /P !TupleFDist.dE big_ord_recl big_ord0 !Uniform.dE mulR1.
 rewrite -big_distrr /= (_ : \sum_(_ | _) _ = 1)%R; last first.
   transitivity (\sum_(i in 'M_1) Binary.d card_A p_01 (i ``_ ord0) a')%R.
     apply eq_bigr => i _.

information_theory/aep.v

@@ -20,7 +20,7 @@ Local Open Scope vec_ext_scope.
 (* properties of the ``- log P'' random variable *)
 Section mlog_prop.
 
-Variables (A : finType) (P : dist A).
+Variables (A : finType) (P : fdist A).
 
 Lemma E_mlog : `E (--log P) = `H P.
 Proof.
@@ -54,12 +54,12 @@ Proof. rewrite -V_mlog /Var; apply Ex_ge0 => ?; exact: pow_even_ge0. Qed.
 
 End mlog_prop.
 
-Definition sum_mlog_prod A (P : dist A) n : {RV (P `^ n) -> R} :=
+Definition sum_mlog_prod A (P : fdist A) n : {RV (P `^ n) -> R} :=
   (fun t => \sum_(i < n) - log (P t ``_ i))%R.
 
 Arguments sum_mlog_prod {A} _ _.
 
-Lemma sum_mlog_prod_sum_map_mlog A (P : dist A) n :
+Lemma sum_mlog_prod_sum_map_mlog A (P : fdist A) n :
   sum_mlog_prod P n.+1 \=sum (\row_(i < n.+1) --log P).
 Proof.
 elim : n => [|n IH].
@@ -84,7 +84,7 @@ Qed.
 
 Section aep_k0_constant.
 
-Variables (A : finType) (P : dist A).
+Variables (A : finType) (P : fdist A).
 
 Definition aep_bound epsilon := (aep_sigma2 P / epsilon ^ 3)%R.
 
@@ -103,7 +103,7 @@ End aep_k0_constant.
 
 Section AEP.
 
-Variables (A : finType) (P : dist A) (n : nat) (epsilon : R).
+Variables (A : finType) (P : fdist A) (n : nat) (epsilon : R).
 Hypothesis Hepsilon : 0 < epsilon.
 
 Lemma aep : aep_bound P epsilon <= INR n.+1 ->
@@ -127,9 +127,9 @@ have {H1 H2} := (wlln (H1 n) (H2 n) Hsum Hepsilon).
 move/(leR_trans _); apply.
 apply/Pr_incl/subsetP => ta; rewrite 2!inE => /andP[H1].
 rewrite /sum_mlog_prod [--log _]lock /= -lock /= /scale_RV /mlog_RV.
-rewrite TupleDist.dE log_rmul_rsum_mlog //.
-apply: (rprodr_gt0_inv (dist_ge0 P)).
-move: H1; by rewrite TupleDist.dE => /ltRP.
+rewrite TupleFDist.dE log_rmul_rsum_mlog //.
+apply: (rprodr_gt0_inv (fdist_ge0 P)).
+move: H1; by rewrite TupleFDist.dE => /ltRP.
 Qed.
 
 End AEP.

information_theory/binary_symmetric_channel.v

@@ -38,7 +38,7 @@ Section bsc_capacity_proof.
 
 Variable A : finType.
 Hypothesis card_A : #|A| = 2%nat.
-Variable P : dist A.
+Variable P : fdist A.
 Variable p : R.
 Hypothesis p_01' : (0 < p < 1)%R.
 
@@ -55,7 +55,7 @@ rewrite {1}/entropy .
 set a := \sum_(_ in _) _. set b := \sum_(_ <- _) _.
 apply trans_eq with (- (a + (-1) * b)); first by field.
 rewrite /b {b} big_distrr /= /a {a} -big_split /=.
-rewrite !Set2sumE /= !JointDistChan.dE /BSC.c !Binary.dE /=.
+rewrite !Set2sumE /= !JointFDistChan.dE /BSC.c !Binary.dE /=.
 rewrite !/Binary.f !eqxx /Binary.f 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.
@@ -64,21 +64,21 @@ case: (Req_EM_T (P a) 0) => H1.
   rewrite H1 add0R => ->.
   rewrite /log Log_1 !(mul0R, mulR0, addR0, add0R, mul1R, mulR1); field.
 rewrite /log LogM; last 2 first.
-  rewrite -dist_gt0; exact/eqP.
+  rewrite -fdist_gt0; exact/eqP.
   case: p_01' => ? ?; lra.
 rewrite /log LogM; last 2 first.
-  rewrite -dist_gt0; exact/eqP.
+  rewrite -fdist_gt0; exact/eqP.
   by case: p_01'.
 case: (Req_EM_T (P b) 0) => H2.
   rewrite H2 !(mul0R, mulR0, addR0, add0R).
   move: (epmf1 P); rewrite Set2sumE /= -/a -/b.
   rewrite H2 addR0 => ->.
   rewrite /log Log_1 !(mul0R, mulR0, addR0, add0R, mul1R, mulR1); field.
 rewrite /log LogM; last 2 first.
-  rewrite -dist_gt0; exact/eqP.
+  rewrite -fdist_gt0; exact/eqP.
   by case: p_01'.
 rewrite /log LogM; last 2 first.
-  rewrite -dist_gt0; exact/eqP.
+  rewrite -fdist_gt0; exact/eqP.
   rewrite subR_gt0; by case: p_01'.
 transitivity (p * (P a + P b) * log p + (1 - p) * (P a + P b) * log (1 - p) ).
   rewrite /log; by field.
@@ -95,17 +95,17 @@ Qed.
 
 Lemma H_out_max : `H(P `o BSC.c card_A p_01) <= 1.
 Proof.
-rewrite {1}/entropy /= Set2sumE /= !OutDist.dE 2!Set2sumE /=.
+rewrite {1}/entropy /= Set2sumE /= !OutFDist.dE 2!Set2sumE /=.
 set a := Set2.a _. set b := Set2.b _.
 rewrite /BSC.c !Binary.dE !eqxx /= !(eq_sym _ a).
 rewrite (negbTE (Set2.a_neq_b card_A)).
 move: (epmf1 P); rewrite Set2sumE /= -/a -/b => P1.
 have -> : p * P a + (1 - p) * P b = 1 - ((1 - p) * P a + p * P b).
   rewrite -{2}P1; by field.
 have H01 : 0 < ((1 - p) * P a + p * P b) < 1.
-  move: (dist_ge0 P a) => H1.
-  move: (dist_max P b) => H4.
-  move: (dist_max P a) => H3.
+  move: (fdist_ge0 P a) => H1.
+  move: (fdist_max P b) => H4.
+  move: (fdist_max P a) => H3.
   case: p_01' => Hp1 Hp2.
   split.
     case/Rle_lt_or_eq_dec : H1 => H1.
@@ -124,7 +124,7 @@ have H01 : 0 < ((1 - p) * P a + p * P b) < 1.
   - apply leR_lt_add.
     + rewrite -{2}(mul1R (P a)); apply leR_wpmul2r; lra.
     + rewrite -{2}(mul1R (P b)); apply ltR_pmul2r => //.
-      apply/ltRP; rewrite lt0R; apply/andP; split; [exact/eqP|exact/leRP/dist_ge0].
+      apply/ltRP; rewrite lt0R; apply/andP; split; [exact/eqP|exact/leRP/fdist_ge0].
   - rewrite -H1 mulR0 2!add0R.
     have -> : P b = 1 by rewrite -P1 -H1 add0R.
     by rewrite mulR1.
@@ -140,7 +140,7 @@ Proof. rewrite /= (_ : INR 1 = 1) // (_ : INR 2 = 2) //; lra. Qed.
 
 Lemma H_out_binary_uniform : `H(Uniform.d card_A `o BSC.c card_A p_01) = 1.
 Proof.
-rewrite {1}/entropy !Set2sumE /= !OutDist.dE !Set2sumE /=.
+rewrite {1}/entropy !Set2sumE /= !OutFDist.dE !Set2sumE /=.
 rewrite /BSC.c !Binary.dE !eqxx (eq_sym _ (Set2.a _)) !Uniform.dE.
 rewrite (negbTE (Set2.a_neq_b card_A)).
 rewrite -!mulRDl (_ : 1 - p + p = 1); last by field.