package rocq-infotheo
Discrete probabilities and information theory for Rocq
Install
Dune Dependency
Authors
-
RReynald Affeldt, AIST
-
MManabu Hagiwara, Chiba U. (previously AIST)
-
JJonas Senizergues, ENS Cachan (internship at AIST)
-
Jacques Garrigue
-
KKazuhiko Sakaguchi, Tsukuba U.
-
TTaku Asai, Nagoya U. (M2)
-
TTakafumi Saikawa, Nagoya U.
-
NNaruomi Obata, Titech (M2)
-
AAlessandro Bruni, IT-University of Copenhagen
Maintainers
Sources
0.9.8.tar.gz
sha512=3e07630736014b6087d660d014b2e6a3440e7d3d13ef058fd532b137d8faffc67f80f826780e6e5dc9995502d60d1f97ef10eb2f2df6bc1f013720f88d520be1
Description
Infotheo is a Rocq library for reasoning about discrete probabilities, information theory, and linear error-correcting codes.
Tags
keyword:information theory keyword:probability keyword:error-correcting codes keyword:convexity logpath:infotheo date:2026-09-20Published: 21 Sep 2026
Dependencies (5)
-
coq-interval
>= "4.11.5" -
rocq-mathcomp-reals-stdlib
(>= "1.18.0") -
rocq-mathcomp-analysis
(>= "1.18.0") -
rocq-mathcomp-algebra
(>= "2.6.0") -
rocq-core
(>= "9.1.1" & < "9.4~")
Dev Dependencies
None
Used by
None
Conflicts
None
On This Page