minor cleaning around random variables - Githubissues

affeldt-aist / infotheo

A Coq formalization of information theory and linear error-correcting codes

GNU Lesser General Public License v2.1

64 stars 15 forks source link

minor cleaning around random variables #68

Closed t6s closed 2 years ago

t6s commented 3 years ago

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.