WIP: use realType in fdists - 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

WIP: use realType in fdists #100

Closed yoshihiro503 closed 1 year ago

yoshihiro503 commented 1 year ago

prograss...

[x] redefinition Module FDist
[x] Section fdist_lemmas
[x] Section fdist1.
[x] Section fdist1_prop.
[x] Section fdistbind.
[x] Section fdistmap.
[x] Section fdistmap_prop.
[x] Section fdist_uniform.
[x] Section fdist_uniform_prop.
[x] Section fdist_uniform_supp.
[x] Section fdist_uniform_supp_prop.
[x] Section fdist_binary.
[x] Section fdist_binary_prop.
[x] Section fdist_binary_supp.
[x] Section fdistD1.
[x] Section fdistD1_prop.
[x] Section fdistI2.
[x] Section fdistI2_prop.
[x] Section fdist_add.
[x] Section fdist_del.
[x] Section fdist_belast.
[x] Section fdist_convn.
[x] Section fdist_convn_prop.
[x] Section fdist_conv.
[x] Section fdist_perm.
[x] Section fdistI_perm.
[x] Section fdistI_perm_prop.
[x] Section fdist_fst_snd.
[x] Section fdist_prod.
[x] Section fdist_prod_prop.
[x] Section prod_dominates_joint.
[x] Section fdistX.
[x] Section fdistX_prop.
[x] Section fdist_rV.
[x] Section wolfowitz_counting.
[x] Section fdist_prod_of_rV.
[x] Section fdist_rV_of_prod.
[x] Section fdist_rV_prop.
[x] Section fdist_col'.
[x] Section fdist_col'_prop.
[x] Section fdist_nth.
[x] Section fdist_nth_prop.
[x] Section fdist_take.
[x] Section fdist_take_prop.
[x] Section fdistA.
[x] Section fdistA_prop.
[x] Section fdistC12.
[x] Section fdistC12_prop.
[x] Section fdistAC.
[x] Section fdistAC_prop.
[x] Section fdistC13.
[x] Section fdist_proj13.
[x] Section fdist_proj23.
[x] Section fdist_self.
[x] Section fdist_self_prop.
[x] Section def.
[x] Section subvec_prop.
[x] Section fdist_prod_nth.
[x] Section fdist_prod_take.
[x] Section to_bivar_last_take.
[x] Section fdist_take_drop.

affeldt-aist commented 1 year ago

This is now superseded by https://github.com/affeldt-aist/infotheo/pull/103