Lebesgue-Stieltjes Integral

Yosuke Ito 📧

March 4, 2026

Abstract

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. \]

License

BSD License

Topics

Session Lebesgue_Stieltjes_Integral

Depends on

Cite

× 
@article{Lebesgue_Stieltjes_Integral-AFP,
  author  = {Yosuke Ito},
  title   = {Lebesgue-Stieltjes Integral},
  journal = {Archive of Formal Proofs},
  month   = {March},
  year    = {2026},
  note    = {\url{https://isa-afp.org/entries/Lebesgue_Stieltjes_Integral.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download