Lebesgue-Stieltjes Integral

Yosuke Ito 📧

March 4, 2026

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

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