Generalize operations of random variables and add bij_RV_unif, etc. #145

weng-chenghui · 2025-03-07T07:16:41Z

Generalize operations of random variables and add trans_RV_unif and neg_RV_unif
Add bij_RV_unif
Fix errors: 1^-1 before this change becomes 1/n (need mul1r)

…d neg_RV_unif 2. Add bij_RV_unifs 3. Fix errors: 1^-1 before this change becomes 1/n (need mul1r)

probability/proba.v

affeldt-aist · 2025-03-08T02:17:10Z

probability/proba.v

+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 *)


I think that it is ok to do the renaming as part of this PR (but it's better be recorded in the changelog).

affeldt-aist · 2025-03-08T02:17:54Z

probability/proba.v

+(* 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 *)


I think that it is ok to remove it, just leave a note in the changelog in case we use it in monae.

affeldt-aist · 2025-03-08T02:18:32Z

probability/proba.v

+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} :=


try remove the seq. prefix

probability/proba.v

affeldt-aist · 2025-03-08T02:20:26Z

probability/proba.v

+Section zmod_random_variables_lemmas.
+
+End zmod_random_variables_lemmas.


Remove the empty section?

probability/proba.v

affeldt-aist · 2025-03-08T02:23:34Z

probability/proba.v

+
+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.


It might be better in practice to write n%:R^-1 instead of 1 / n%:R (maybe leave a note in the changlog).

probability/proba.v

affeldt-aist

This generalization is an improvement. I commited a few, trivial cosmetics changes but I left a couple of easy comments that'd better be taken care of within this PR imo.

1. Generalize operations of random variables and add trans_RV_unif an…

2479f4e

…d neg_RV_unif 2. Add bij_RV_unifs 3. Fix errors: 1^-1 before this change becomes 1/n (need mul1r)

weng-chenghui mentioned this pull request Mar 7, 2025

Generalize operations of random variables and add trans_RV_unif and neg_RV_unif #135

Open

weng-chenghui marked this pull request as ready for review March 7, 2025 07:17

weng-chenghui changed the title ~~Generalize operations of random variables and add bij_RV_unifs, etc.~~ Generalize operations of random variables and add bij_RV_unif, etc. Mar 7, 2025