In this article, the basic existence theorem of Riemann-Stieltjes integral is formalized. This theorem states that if f is a continuous function and ρ is a function of bounded variation in a closed interval of real line, f is Riemann-Stieltjes integrable with respect to ρ. In the first section, basic properties of real finite sequences are formalized as preliminaries. In the second section, we formalized the existence theorem of the Riemann-Stieltjes integral. These formalizations are based on [15], [12], [10], and [11].
@article{bwmeta1.element.doi-10_1515_forma-2016-0021,
author = {Kazuhisa Nakasho and Keiko Narita and Yasunari Shidama},
title = {The Basic Existence Theorem of Riemann-Stieltjes Integral},
journal = {Formalized Mathematics},
volume = {24},
year = {2016},
pages = {253-259},
zbl = {1357.26014},
language = {en},
url = {http://dml.mathdoc.fr/item/bwmeta1.element.doi-10_1515_forma-2016-0021}
}
Kazuhisa Nakasho; Keiko Narita; Yasunari Shidama. The Basic Existence Theorem of Riemann-Stieltjes Integral. Formalized Mathematics, Tome 24 (2016) pp. 253-259. http://gdmltest.u-ga.fr/item/bwmeta1.element.doi-10_1515_forma-2016-0021/