coq-markov

Markov's inequality. A proof of Markov's inequality, restricted to probability spaces, based on the Wikipedia proof. Defines Lebesgue integral and associated concepts such as measurability, measure functions, and sigma algebras. Extended real numbers did not need to be defined because we are working in a probability space with measure 1. Nonconstructive; uses classic, Extensionality_Ensembles, axiomatized real numbers from Coq standard library.

opam install coq-markov.8.5.0
homepage
https://github.com/coq-contribs/markov
license
GNU Lesser Public License
bugs tracker
https://github.com/coq-contribs/markov/issues
dependencies
coq (>= 8.5 & < 8.6~)
source
https://github.com/coq-contribs/markov/archive/v8.5.0.tar.gz
package
https://github.com/coq/opam-coq-archive/tree/master/released/packages/coq-markov/coq-markov.8.5.0