New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

minor cleaning around random variables #68

Merged

affeldt-aist merged 3 commits into master from tidy_RV

Oct 25, 2021

Collaborator

t6s commented Oct 21, 2021

I have separated some easy parts from draft #67 :

added:

in ssrR.v:
- lemmas ltR0Sn, lt0n_neqR0, lt0n_neqR0'
in proba.v
- lemmas scalel_RVA, scaler_RVA, sq_RV_pow2, sq_RV_ge0, E_trans_min_RV

removed:

in aep.v
- lemma E_mlog (since it is equivalent to entropy.entropy_Ex)

changed:

in aep.v
- a cleaner expression for aep_sigma2
in proba.v
- stopped importing the unused Nsatz

I have also added some header comments in entropy.v.

t6s and others added 3 commits

October 21, 2021 22:34


          minor cleanup around RVs; also add some ssrR lemmas

2c45c8e


          changelog

7b2377c


          minor fixes, add one ssrR lemma

e878f30

affeldt-aist self-requested a review

October 25, 2021 00:33

affeldt-aist approved these changes

View reviewed changes

Owner

affeldt-aist left a comment

Thanks!

affeldt-aist merged commit 56a667c into master

affeldt-aist deleted the tidy_RV branch

December 28, 2021 14:05

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet