Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Lebesgue-Stieltjes Integral

Email Gateway (Mar 20 2026 at 17:00):

From: Manuel Eberl <manuel@pruvisto.org>

Lebesgue-Stieltjes Integral
by Yosuke Ito

This entry formalizes some basic facts and lemmas relating to the
integration with respect to the Lebesgue-Stieltjes measure (interval
measure). It includes the well-known formula to calculate the
Lebesgue-Stieltjes integral: \int g(x) dF(x) = \int g(x) F'(x) dx

https://www.isa-afp.org/entries/Lebesgue_Stieltjes_Integral.html

Enjoy!

Manuel

Last updated: Mar 21 2026 at 20:30 UTC