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)

書誌事項

タイトル別名
  • The Radon-Nikodym Theorem and the Lebesgue-Stieltjes Measure in Coq

この論文をさがす

説明

<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>

収録刊行物

詳細情報 詳細情報について

問題の指摘

ページトップへ