Generalize operations of random variables and add trans_RV_unif and neg_RV_unif

probability/proba.v

@@ -1,6 +1,6 @@
 (* 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 matrix lra.
+From mathcomp Require Import all_ssreflect all_algebra fingroup lra.
 From mathcomp Require boolp.
 From mathcomp Require Import reals exp.
 Require Import realType_ext realType_logb ssr_ext ssralg_ext.
@@ -596,35 +596,77 @@ Section random_variables.
 Context {R : realType}.
 Variables (U : finType) (P : R.-fdist U).
 
+Definition unit_RV : {RV P -> unit} := fun=> tt.
 Definition const_RV (T : eqType) cst : {RV P -> T} := fun=> cst.
 Definition comp_RV (TA TB : eqType) (f : TA -> TB) (X : {RV P -> TA}) : {RV P -> TB} :=
   fun x => f (X x).
-Local Notation "f `o X" := (comp_RV f X).
-Definition scalel_RV k (X : {RV P -> R}) : {RV P -> R} := fun x => k * X x.
-Definition scaler_RV (X : {RV P -> R}) k : {RV P -> R} := fun x => X x * k.
-Definition add_RV (X Y : {RV P -> R}) : {RV P -> R} := fun x => X x + Y x.
-Definition sumR_RV I (r : seq.seq I) (p : pred I) (X : I -> {RV P -> R}) : {RV P -> R} :=
-  fun x => \sum_(i <- r | p i) X i x.
-Definition sub_RV (X Y : {RV P -> R}) : {RV P -> R} := fun x => X x - Y x.
-Definition trans_add_RV (X : {RV P -> R}) m : {RV P -> R} := fun x => X x + m.
-Definition trans_min_RV (X : {RV P -> R}) m : {RV P -> R} := fun x => X x - m.
-Definition sq_RV (X : {RV P -> R}) : {RV P -> R} := (fun x => x ^+ 2) `o X.
-Definition neg_RV (X : {RV P -> R}) : {RV P -> R} := fun x => - X x.
-Definition log_RV : {RV P -> R} := fun x => log (P x).
-Definition unit_RV : {RV P -> unit} := fun=> tt.
 
 End random_variables.
 
-Notation "k `cst* X" := (scalel_RV k X) : proba_scope.
-Notation "X `*cst k" := (scaler_RV X k) : proba_scope.
-Notation "f `o X" := (comp_RV f X) : proba_scope.
-Notation "X '`/' n" := (scalel_RV (1 / n%:R) X) : proba_scope.
+Notation "f `o X" := (comp_RV f X).
+
+Section zmod_random_variables.
+Context {R : realType}.
+Local Open Scope ring_scope.
+
+Variables (U : finType)(P : R.-fdist U)(V : zmodType).
+
+Definition add_RV (X Y : {RV P -> V}) : {RV P -> V} := fun x => X x + Y x.
+Definition sub_RV (X Y : {RV P -> V}) : {RV P -> V} := fun x => X x - Y x.
+
+(* TODO: neg to opp *)
+Definition neg_RV (X : {RV P -> V}) : {RV P -> V} := fun x => - X x.
+Definition trans_add_RV (X : {RV P -> V}) m : {RV P -> V} := fun x => X x + m.
+(* TODO: min to sub; no longer necessary *)
+Definition trans_min_RV (X : {RV P -> V}) m : {RV P -> V} := fun x => X x - m.
+Definition sumR_RV I (r : seq.seq I) (p : pred I) (X : I -> {RV P -> V}) : {RV P -> V} :=
+  fun x => \sum_(i <- r | p i) X i x.
+
+Local Notation "X `+ Y" := (add_RV X Y) : proba_scope.
+Local Notation "X `- Y" := (sub_RV X Y) : proba_scope.
+
+Lemma sub_RV_neg  (X Y : {RV P -> V}):
+  X `- Y = X `+ neg_RV Y.
+Proof. by []. Qed.
+
+End zmod_random_variables.
+
 Notation "X `+ Y" := (add_RV X Y) : proba_scope.
 Notation "X `- Y" := (sub_RV X Y) : proba_scope.
 Notation "X '`+cst' m" := (trans_add_RV X m) : proba_scope.
 Notation "X '`-cst' m" := (trans_min_RV X m) : proba_scope.
-Notation "X '`^2' " := (sq_RV X) : proba_scope.
 Notation "'`--' P" := (neg_RV P) : proba_scope.
+
+Section zmod_random_variables_lemmas.
+
+End zmod_random_variables_lemmas.
+
+Section ring_random_variables.
+Context {R : realType}.
+Local Open Scope ring_scope.
+
+Variables (U : finType)(P : R.-fdist U)(V : ringType).
+
+Definition scalel_RV k (X : {RV P -> V}) : {RV P -> V} := fun x => k * X x.
+Definition scaler_RV (X : {RV P -> V}) k : {RV P -> V} := fun x => X x * k.
+Definition sq_RV (X : {RV P -> V}) : {RV P -> V} := (fun x => x ^+ 2) `o X.
+
+End ring_random_variables.
+
+Notation "k `cst* X" := (scalel_RV k X) : proba_scope.
+Notation "X `*cst k" := (scaler_RV X k) : proba_scope.
+Notation "X '`/' n" := (scalel_RV (1 / n%:R) X) : proba_scope.
+Notation "X '`^2' " := (sq_RV X) : proba_scope.
+
+Section real_random_variables.
+Context {R : realType}.
+
+Variables (U : finType)(P : R.-fdist U).
+
+Definition log_RV : {RV P -> R} := fun x => log (P x).
+
+End real_random_variables.
+
 Notation "'`log' P" := (log_RV P) : proba_scope.
 
 Section RV_lemmas.
@@ -1340,6 +1382,52 @@ Qed.
 
 End mutual_independence.
 
+Section uniform_finType_RV_lemmas.
+Local Open Scope proba_scope.
+Context {R : realType}.
+Variables (T: finType) (n: nat) (P : R.-fdist T) (A : finType).
+Variable X : {RV P -> A}.
+
+Hypothesis card_A : #|A| = n.+1.
+Hypothesis Xunif : `p_X = fdist_uniform card_A.
+
+Lemma bij_comp_RV (f g : A -> A) :
+  cancel f g -> cancel g f -> `p_(f `o X) =1 `p_X \o g.
+Proof.
+move=> fg gf x /=; rewrite !fdistbindE.
+apply: eq_bigr=> a _.
+by rewrite !fdist1E -(can_eq gf) fg.
+Qed.
+
+Lemma bij_RV_unif (f g : A -> A) :
+  cancel f g -> cancel g f -> `p_(f `o X) = fdist_uniform card_A.
+Proof.
+move => fg gf.
+apply/val_inj/ffunP => x /=.
+by rewrite (bij_comp_RV fg gf) Xunif /= !fdist_uniformE.
+Qed.
+
+End uniform_finType_RV_lemmas.
+
+Section uniform_finZmod_RV_lemmas.
+Local Open Scope proba_scope.
+Context {R : realType}.
+Variables (T: finType) (P : R.-fdist T) (A : finZmodType).
+Variable X : {RV P -> A}.
+
+Let n := #|A|.-1.
+Let card_A : #|A| = n.+1.
+Proof. by apply/esym/prednK/card_gt0P; exists 0. Qed.
+
+Hypothesis Xunif : `p_X = fdist_uniform card_A.
+
+Lemma trans_RV_unif (m : A) : `p_(X `+cst m) = fdist_uniform card_A.
+Proof. exact: (bij_RV_unif Xunif (addrK m) (subrK m)). Qed.
+
+Lemma neg_RV_unif : `p_(`-- X) = fdist_uniform card_A.
+Proof. exact: (bij_RV_unif Xunif opprK opprK). Qed.
+End uniform_finZmod_RV_lemmas.
+
 Section conditional_probablity.
 Context {R : realType}.
 Variables (A : finType) (d : R.-fdist A).