The Radon-Nikodým Theorem and the Lebesgue-Stieltjes Measure in Coq

DOI Web Site
  • ISHIGURO Yoshihiro
    Graduate School of Mathematics, Nagoya University
  • AFFELDT Reynald
    Digital Architecture Research Center,National Institute of Advanced Industrial Science and Technology (AIST)

Bibliographic Information

Other Title
  • The Radon-Nikodym Theorem and the Lebesgue-Stieltjes Measure in Coq

Search this article

Description

<p>We are concerned with the formalization of measure theory in the Coq proof assistant. Concretely, we extend MathComp-Analysis, a library for functional analysis built on top of the Mathematical Components library, with standard constructions such as charges and the Lebesgue-Stieltjes measure, and with standard theorems such as the Hahn decomposition theorem and the Radon-Nikodým theorem. These are prerequisites for the formalization of probabilistic programs, of probability theory, and also for other applications such as the formalization of connections between derivatives and integrals.</p>

Journal

  • Computer Software

    Computer Software 41 (2), 2_41-2_59, 2024-04-23

    Japan Society for Software Science and Technology

Details 詳細情報について

Report a problem

Back to top